--- a/src/Provers/Arith/abel_cancel.ML Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Fri Oct 21 18:14:34 2005 +0200
@@ -90,7 +90,7 @@
fun sum_proc sg ss t =
let val t' = cancel sg t
- val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
+ val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t'))
(fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
in SOME thm end
handle Cancel => NONE;
@@ -110,7 +110,7 @@
fun rel_proc sg ss t =
let val t' = cancel sg t
- val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
+ val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t'))
(fn _ => rtac eq_reflection 1 THEN
resolve_tac eqI_rules 1 THEN
simp_tac (Simplifier.inherit_context ss cancel_ss) 1)