diff -r 532b915afa14 -r 1ebb8b7b9f6a src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 29 12:50:44 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 29 15:16:54 2009 +0100
@@ -197,7 +197,7 @@
               else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
           in
             rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
-            THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac)
+            THEN (if tag_flag then Arith_Data.arith_tac ctxt 1 else all_tac)
           end
 
         fun steps_tac MAX strict lq lp =