# HG changeset patch
# User nipkow
# Date 1029268913 -7200
# Node ID 79242cccaddcd7ed50134742f0f7fc3403733b0b
# Parent  2222c7a0e8bb80d0fbbae7e22287ca3042b70609
arith_tac should not produce counter example

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 []};