src/HOL/Tools/Function/scnp_reconstruct.ML

             val rule = if strict
               then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
               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 =
           let
             val (empty, step) = ord_intros_max strict