src/HOL/Tools/TFL/post.ML

--- a/src/HOL/Tools/TFL/post.ML	Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Tue Jul 31 00:56:26 2007 +0200
@@ -68,7 +68,7 @@
   Prim.postprocess strict
    {wf_tac     = REPEAT (ares_tac wfs 1),
     terminator = asm_simp_tac ss 1
-                 THEN TRY (silent_arith_tac 1 ORELSE
+                 THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE
                            fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1),
     simplifier = Rules.simpl_conv ss []};