--- a/src/Provers/Arith/fold_Suc.ML Fri Apr 28 10:44:03 2000 +0200
+++ b/src/Provers/Arith/fold_Suc.ML Fri Apr 28 10:44:20 2000 +0200
@@ -18,7 +18,7 @@
(*proof tools*)
val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
val add_norm_tac: tactic
- val numeral_simp_tac: thm list -> tactic
+ val numeral_simp_tac: tactic
end;
@@ -42,7 +42,7 @@
(sum, Data.mk_sum (lit_m::terms')))
in
Data.prove_conv
- [Data.numeral_simp_tac assocs] sg
+ [rewrite_goals_tac assocs, Data.numeral_simp_tac] sg
(t, Data.mk_sum (Data.mk_numeral (m+1) :: terms'))
end
handle TERM _ => None;