# HG changeset patch
# User nipkow
# Date 1008258487 -3600
# Node ID 83acab8042add8bb290c895b398d38ef0618e280
# Parent  bbd564190c9bb2a5a94aaeeab72a85897bb790f2
Terminator now uses arith_tac as well.

diff -r bbd564190c9b -r 83acab8042ad TFL/post.ML
--- a/TFL/post.ML	Thu Dec 13 16:47:35 2001 +0100
+++ b/TFL/post.ML	Thu Dec 13 16:48:07 2001 +0100
@@ -71,7 +71,8 @@
   Prim.postprocess strict
    {wf_tac     = REPEAT (ares_tac wfs 1),
     terminator = asm_simp_tac ss 1
-                 THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
+                 THEN TRY (arith_tac 1 ORELSE
+                           fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
     simplifier = Rules.simpl_conv ss []};