diff -r 3b34516662c6 -r 369e2af8ee45 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Provers/quantifier1.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -104,7 +104,7 @@
   in exqu end;
 
 fun prove_conv tac thy tu =
-  Tactic.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
+  Goal.prove 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)