From 65b818146effe2f74192a3b1d65b4ec792a8a350 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Thu, 17 Oct 2013 09:22:38 -0400
Subject: Save disjointness environments across top-level declarations

---
 src/elaborate.sml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

(limited to 'src/elaborate.sml')

diff --git a/src/elaborate.sml b/src/elaborate.sml
index ace7a758..ff5a3b95 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -4002,6 +4002,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                                  end
 
                          val (env', n) = E.pushStrNamed env x sgn'
+
                          val denv' =
                              case #1 str' of
                                  L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
@@ -4581,16 +4582,12 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
 
         val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
 
-        fun elabDecl' (d, (env, gs)) =
-            let
-                val () = resetKunif ()
-                val () = resetCunif ()
-                val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs))
-            in
-                (ds, (env', gs))
-            end
+        fun elabDecl' x =
+            (resetKunif ();
+             resetCunif ();
+             elabDecl x)
 
-        val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
+        val (file, (env'', _, gs)) = ListUtil.foldlMapConcat elabDecl' (env', D.empty, []) file
 
         fun oneSummaryRound () =
             if ErrorMsg.anyErrors () then
-- 
cgit v1.2.3