--- a/src/elaborate.sml	Sun Apr 12 10:08:11 2009 -0400
+++ b/src/elaborate.sml	Sun Apr 12 11:08:00 2009 -0400
@@ -3284,30 +3284,40 @@
                                                      (L'.CApp (tf, arg), _) =>
                                                      (case (hnormCon env tf, hnormCon env arg) of
                                                           ((L'.CModProj (basis, [], "transaction"), _),
-                                                           (L'.CApp (tf, arg3), _)) =>
+                                                           (L'.CApp (tf, arg4), _)) =>
                                                           (case (basis = !basis_r,
-                                                                 hnormCon env tf, hnormCon env arg3) of
+                                                                 hnormCon env tf, hnormCon env arg4) of
                                                                (true,
-                                                                (L'.CApp (tf, arg2), _),
+                                                                (L'.CApp (tf, arg3), _),
                                                                 ((L'.CRecord (_, []), _))) =>
-                                                               (case (hnormCon env tf) of
-                                                                    (L'.CApp (tf, arg1), _) =>
-                                                                    (case (hnormCon env tf,
-                                                                           hnormCon env arg1,
-                                                                           hnormCon env arg2) of
-                                                                         (tf, arg1,
-                                                                          (L'.CRecord (_, []), _)) =>
-                                                                         let
-                                                                             val t = (L'.CApp (tf, arg1), loc)
-                                                                             val t = (L'.CApp (t, arg2), loc)
-                                                                             val t = (L'.CApp (t, arg3), loc)
-                                                                             val t = (L'.CApp (
-                                                                                      (L'.CModProj
-                                                                                           (basis, [], "transaction"), loc),
+                                                               (case hnormCon env tf of
+                                                                    (L'.CApp (tf, arg2), _) =>
+                                                                    (case hnormCon env tf of
+                                                                         (L'.CApp (tf, arg1), _) =>
+                                                                         (case (hnormCon env tf,
+                                                                                hnormCon env arg1,
+                                                                                hnormCon env arg2,
+                                                                                hnormCon env arg3,
+                                                                                hnormCon env arg4) of
+                                                                              (tf,
+                                                                               arg1,
+                                                                               (L'.CRecord (_, []), _),
+                                                                               arg2,
+                                                                               arg4) =>
+                                                                              let
+                                                                                  val t = (L'.CApp (tf, arg1), loc)
+                                                                                  val t = (L'.CApp (t, arg2), loc)
+                                                                                  val t = (L'.CApp (t, arg3), loc)
+                                                                                  val t = (L'.CApp (t, arg4), loc)
+
+                                                                                  val t = (L'.CApp (
+                                                                                           (L'.CModProj
+                                                                                                (basis, [], "transaction"), loc),
                                                                                       t), loc)
-                                                                         in
-                                                                             (L'.SgiVal (x, n, makeRes t), loc)
-                                                                         end
+                                                                              in
+                                                                                  (L'.SgiVal (x, n, makeRes t), loc)
+                                                                              end
+                                                                            | _ => all)
                                                                        | _ => all)
                                                                   | _ => all)
                                                              | _ => all)
@@ -3622,6 +3632,16 @@
                      [] => ()
                    | _ => raise Fail "Unresolved disjointness constraints in top.urs"
         val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
+
+        val () = subSgn env' topSgn' topSgn
+
+        val () = app (fn (env, k, s1, s2) =>
+                         unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
+                         handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in Top final record unification";
+                                                cunifyError env err))
+                     (!delayedUnifs)
+        val () = delayedUnifs := []
+
         val () = case gs of
                      [] => ()
                    | _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
@@ -3631,7 +3651,8 @@
                                        (prefaces "Unresolved constraint in top.ur"
                                                  [("loc", PD.string (ErrorMsg.spanToString loc)),
                                                   ("c1", p_con env c1),
-                                                  ("c2", p_con env c2)];
+                                                  ("c2", p_con env c2),
+                                                  ("topStr", p_str env topStr)];
                                         raise Fail "Unresolved constraint in top.ur"))
                                 | TypeClass (env, c, r, loc) =>
                                   let
@@ -3642,8 +3663,6 @@
                                         | NONE => expError env (Unresolvable (loc, c))
                                   end) gs
 
-        val () = subSgn env' topSgn' topSgn
-
         val (env', top_n) = E.pushStrNamed env' "Top" topSgn
         val () = top_r := top_n