--- 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)