src/Tools/eqsubst.ML
changeset 58950 d07464875dd4
parent 58838 59203adfc33f
child 59498 50b60f501b05
     1.1 --- a/src/Tools/eqsubst.ML	Sat Nov 08 17:39:01 2014 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Sat Nov 08 21:31:51 2014 +0100
     1.3 @@ -161,7 +161,7 @@
     1.4               Vartab.dest (Envir.term_env env));
     1.5            val initenv =
     1.6              Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
     1.7 -          val useq = Unify.smash_unifiers thy [a] initenv
     1.8 +          val useq = Unify.smash_unifiers (Context.Theory thy) [a] initenv
     1.9              handle ListPair.UnequalLengths => Seq.empty
    1.10                | Term.TERM _ => Seq.empty;
    1.11            fun clean_unify' useq () =