diff -r 2222c7a0e8bb -r 79242cccaddc TFL/post.ML
--- a/TFL/post.ML	Tue Aug 13 21:59:44 2002 +0200
+++ b/TFL/post.ML	Tue Aug 13 22:01:53 2002 +0200
@@ -71,7 +71,7 @@
   Prim.postprocess strict
    {wf_tac     = REPEAT (ares_tac wfs 1),
     terminator = asm_simp_tac ss 1
-                 THEN TRY (arith_tac 1 ORELSE
+                 THEN TRY (silent_arith_tac 1 ORELSE
                            fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
     simplifier = Rules.simpl_conv ss []};