diff -r e2e6b0691264 -r a6a6e8031c14 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Tools/eqsubst.ML	Fri Jul 17 21:33:00 2009 +0200
@@ -231,9 +231,9 @@
          or should I be using them somehow? *)
           fun mk_insts env =
             (Vartab.dest (Envir.type_env env),
-             Envir.alist_of env);
-          val initenv = Envir.Envir {asol = Vartab.empty,
-                                     iTs = typinsttab, maxidx = ix2};
+             Vartab.dest (Envir.term_env env));
+          val initenv =
+            Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
           val useq = Unify.smash_unifiers thry [a] initenv
 	            handle UnequalLengths => Seq.empty
 		               | Term.TERM _ => Seq.empty;