changeset 12488 | 83acab8042ad |
parent 12341 | 08afd1003151 |
child 13501 | 79242cccaddc |
--- 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 []};