changeset 20049 | f48c4a3a34bc |
parent 17956 | 369e2af8ee45 |
child 31166 | a90fe83f58ea |
--- a/src/Provers/quantifier1.ML Sat Jul 08 12:54:36 2006 +0200 +++ b/src/Provers/quantifier1.ML Sat Jul 08 12:54:37 2006 +0200 @@ -104,7 +104,8 @@ in exqu end; fun prove_conv tac thy tu = - Goal.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac)); + Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu) + (K (rtac iff_reflection 1 THEN tac)); fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)