From 9546f78b908f9571b1cc2b70c5d6e1da646719d7 Mon Sep 17 00:00:00 2001
From: Nishant Kheterpal <nishantkheterpal@gmail.com>
Date: Wed, 22 May 2024 15:13:53 -0500
Subject: [PATCH] theorem now elaborates to in-part

---
 src/haz3lcore/dynamics/Elaborator.re | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index a3fb151d11..4027ee9d25 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -200,7 +200,7 @@ let rec dhexp_of_uexp =
       | Test(test) =>
         let+ dtest = dhexp_of_uexp(m, test);
         DHExp.Test(id, dtest);
-      | Theorem(_, _, _) => Some(DHExp.Tuple([]))
+      | Theorem(_, _, e) => dhexp_of_uexp(m, e)
       | Filter(act, cond, body) =>
         let* dcond = dhexp_of_uexp(~in_filter=true, m, cond);
         let+ dbody = dhexp_of_uexp(m, body);