src/Pure/Proof/extraction.ML
changeset 58950 d07464875dd4
parent 58843 521cea5fa777
child 59058 a78612c67ec0
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Nov 08 17:39:01 2014 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Nov 08 21:31:51 2014 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4            val env' = Envir.Envir
     1.5              {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
     1.6               tenv = tenv, tyenv = Tenv};
     1.7 -          val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
     1.8 +          val env'' = fold (Pattern.unify (Context.Theory thy) o pairself (lookup rew)) prems' env';
     1.9          in SOME (Envir.norm_term env'' (inc (ren tm2)))
    1.10          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
    1.11            (sort (int_ord o pairself fst)