src/Provers/quantifier1.ML
changeset 13480 bb72bd43c6c3
parent 12523 0d8d5bf549b0
child 15027 d23887300b96
--- a/src/Provers/quantifier1.ML	Thu Aug 08 23:42:49 2002 +0200
+++ b/src/Provers/quantifier1.ML	Thu Aug 08 23:46:09 2002 +0200
@@ -104,12 +104,7 @@
   in exqu end;
 
 fun prove_conv tac sg tu =
-  let val meta_eq = cterm_of sg (Logic.mk_equals tu)
-  in prove_goalw_cterm [] meta_eq (K [rtac iff_reflection 1, tac])
-     handle ERROR =>
-            error("The error(s) above occurred while trying to prove " ^
-                  string_of_cterm meta_eq)
-  end;
+  Tactic.prove sg [] [] (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)