src/HOL/Tools/function_package/scnp_reconstruct.ML
changeset 30686 47a32dd1b86e
parent 30607 c3d1590debd8
child 31242 ed40b987a474
     1.1 --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon Mar 23 19:01:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon Mar 23 19:01:16 2009 +0100
     1.3 @@ -197,7 +197,7 @@
     1.4                else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
     1.5            in
     1.6              rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
     1.7 -            THEN (if tag_flag then arith_tac ctxt 1 else all_tac)
     1.8 +            THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac)
     1.9            end
    1.10  
    1.11          fun steps_tac MAX strict lq lp =