# HG changeset patch
# User nipkow
# Date 1282042183 -7200
# Node ID 6e7f8121b4f73cd74afd26c5c30a77ba00d82599
# Parent  4c065e97ecee6cb6aafe1f492878adcd6f90e3b6# Parent  abc655166d615f5d95b822561469e9dcfbd50b9d
merged

diff -r 4c065e97ecee -r 6e7f8121b4f7 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Tue Aug 17 12:30:31 2010 +0200
+++ b/src/Provers/quantifier1.ML	Tue Aug 17 12:49:43 2010 +0200
@@ -113,8 +113,13 @@
   in exqu [] end;
 
 fun prove_conv tac thy tu =
-  Goal.prove (ProofContext.init_global thy) [] [] (Logic.mk_equals tu)
-    (K (rtac iff_reflection 1 THEN tac));
+  let val ctxt = ProofContext.init_global thy;
+      val eq_tu = Logic.mk_equals tu;
+      val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt;
+      val thm = Goal.prove ctxt' [] [] fixed_goal
+            (K (rtac iff_reflection 1 THEN tac));
+      val [gen_thm] = Variable.export ctxt' ctxt [thm];
+  in gen_thm end;
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)