src/HOL/Tools/TFL/post.ML

--- a/src/HOL/Tools/TFL/post.ML	Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Fri May 13 22:55:00 2011 +0200
@@ -40,7 +40,7 @@
     terminator =
       asm_simp_tac (simpset_of ctxt) 1
       THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
-        fast_tac (claset_of ctxt addSDs [@{thm not0_implies_Suc}] addss (simpset_of ctxt)) 1),
+        fast_simp_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
     simplifier = Rules.simpl_conv (simpset_of ctxt) []};