--- a/src/Pure/Proof/reconstruct.ML Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/Proof/reconstruct.ML Sat Nov 08 21:31:51 2014 +0100
@@ -121,7 +121,7 @@
val t' = mk_abs Ts t;
val u' = mk_abs Ts u
in
- (prop, prf, cs, Pattern.unify thy (t', u') env, vTs)
+ (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs)
handle Pattern.Pattern =>
let val (cs', env') = decompose thy [] (t', u') env
in (prop, prf, cs @ cs', env', vTs) end
@@ -263,7 +263,7 @@
val tn2 = Envir.norm_term bigenv t2
in
if Pattern.pattern tn1 andalso Pattern.pattern tn2 then
- (Pattern.unify thy (tn1, tn2) env, ps) handle Pattern.Unif =>
+ (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps) handle Pattern.Unif =>
cantunify thy (tn1, tn2)
else
let val (cs', env') = decompose thy [] (tn1, tn2) env