src/HOL/Tools/TFL/post.ML

--- a/src/HOL/Tools/TFL/post.ML	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Mon Sep 12 07:55:43 2011 +0200
@@ -40,7 +40,7 @@
     terminator =
       asm_simp_tac (simpset_of ctxt) 1
       THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
-        fast_simp_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
+        fast_force_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
     simplifier = Rules.simpl_conv (simpset_of ctxt) []};