# HG changeset patch
# User blanchet
# Date 1256825814 -3600
# Node ID 1ebb8b7b9f6afe73f644922ef2c1a07677c2f96e
# Parent  532b915afa1435028884cec907a4137bff36a8a6
make "sizechange_tac" slightly less verbose

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 =