# HG changeset patch
# User paulson
# Date 956911460 -7200
# Node ID bfba27f0eccfca18946f739659238d65f98f92b1
# Parent  ebb07113c4f79e36d0c9ca3f3b1201b8c418e175
signature change

diff -r ebb07113c4f7 -r bfba27f0eccf src/Provers/Arith/fold_Suc.ML
--- 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;