1.1 --- a/src/Tools/eqsubst.ML	Fri Jul 17 21:33:00 2009 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Fri Jul 17 21:33:00 2009 +0200
     1.3 @@ -231,9 +231,9 @@
     1.4           or should I be using them somehow? *)
     1.5            fun mk_insts env =
     1.6              (Vartab.dest (Envir.type_env env),
     1.7 -             Envir.alist_of env);
     1.8 -          val initenv = Envir.Envir {asol = Vartab.empty,
     1.9 -                                     iTs = typinsttab, maxidx = ix2};
    1.10 +             Vartab.dest (Envir.term_env env));
    1.11 +          val initenv =
    1.12 +            Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
    1.13            val useq = Unify.smash_unifiers thry [a] initenv
    1.14  	            handle UnequalLengths => Seq.empty
    1.15  		               | Term.TERM _ => Seq.empty;