1.1 --- a/src/Provers/quantifier1.ML	Tue Aug 17 12:30:31 2010 +0200
     1.2 +++ b/src/Provers/quantifier1.ML	Tue Aug 17 12:49:43 2010 +0200
     1.3 @@ -113,8 +113,13 @@
     1.4    in exqu [] end;
     1.5  
     1.6  fun prove_conv tac thy tu =
     1.7 -  Goal.prove (ProofContext.init_global thy) [] [] (Logic.mk_equals tu)
     1.8 -    (K (rtac iff_reflection 1 THEN tac));
     1.9 +  let val ctxt = ProofContext.init_global thy;
    1.10 +      val eq_tu = Logic.mk_equals tu;
    1.11 +      val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt;
    1.12 +      val thm = Goal.prove ctxt' [] [] fixed_goal
    1.13 +            (K (rtac iff_reflection 1 THEN tac));
    1.14 +      val [gen_thm] = Variable.export ctxt' ctxt [thm];
    1.15 +  in gen_thm end;
    1.16  
    1.17  fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
    1.18