# HG changeset patch
# User haftmann
# Date 1316264935 -7200
# Node ID 8ae418dfe5618f3571da3f690e1dad275482ed30
# Parent  64469ea4373580d1ed1ae2a7382d89df8144ae68
dropped unused argument – avoids problem with SML/NJ

diff -r 64469ea43735 -r 8ae418dfe561 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Sep 17 00:40:27 2011 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Sep 17 15:08:55 2011 +0200
@@ -148,7 +148,7 @@
   val mk_coeff = mk_coeff
   val dest_coeff = dest_coeff
   val find_first_coeff = find_first_coeff []
-  val trans_tac = K Numeral_Simprocs.trans_tac
+  val trans_tac = Numeral_Simprocs.trans_tac
 
   val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
     [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
@@ -233,7 +233,7 @@
   val dest_coeff = dest_coeff
   val left_distrib = @{thm left_add_mult_distrib} RS trans
   val prove_conv = Arith_Data.prove_conv_nohyps
-  val trans_tac = K Numeral_Simprocs.trans_tac
+  val trans_tac = Numeral_Simprocs.trans_tac
 
   val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac}
   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
@@ -259,7 +259,7 @@
 struct
   val mk_coeff = mk_coeff
   val dest_coeff = dest_coeff
-  val trans_tac = K Numeral_Simprocs.trans_tac
+  val trans_tac = Numeral_Simprocs.trans_tac
 
   val norm_ss1 = Numeral_Simprocs.num_ss addsimps
     numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
@@ -361,7 +361,7 @@
   val mk_coeff = mk_coeff
   val dest_coeff = dest_coeff
   val find_first = find_first_t []
-  val trans_tac = K Numeral_Simprocs.trans_tac
+  val trans_tac = Numeral_Simprocs.trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq
diff -r 64469ea43735 -r 8ae418dfe561 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Sat Sep 17 00:40:27 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Sep 17 15:08:55 2011 +0200
@@ -214,7 +214,7 @@
   val mk_coeff = mk_coeff
   val dest_coeff = dest_coeff 1
   val find_first_coeff = find_first_coeff []
-  val trans_tac = K trans_tac
+  val trans_tac = trans_tac
 
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -289,7 +289,7 @@
   val dest_coeff = dest_coeff 1
   val left_distrib = @{thm combine_common_factor} RS trans
   val prove_conv = Arith_Data.prove_conv_nohyps
-  val trans_tac = K trans_tac
+  val trans_tac = trans_tac
 
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -315,7 +315,7 @@
   val dest_coeff = dest_fcoeff 1
   val left_distrib = @{thm combine_common_factor} RS trans
   val prove_conv = Arith_Data.prove_conv_nohyps
-  val trans_tac = K trans_tac
+  val trans_tac = trans_tac
 
   val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
   fun norm_tac ss =
@@ -365,7 +365,7 @@
 struct
   val mk_coeff = mk_coeff
   val dest_coeff = dest_coeff 1
-  val trans_tac = K trans_tac
+  val trans_tac = trans_tac
 
   val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
   val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
@@ -507,7 +507,7 @@
   val mk_coeff = mk_coeff
   val dest_coeff = dest_coeff
   val find_first = find_first_t []
-  val trans_tac = K trans_tac
+  val trans_tac = trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq 
diff -r 64469ea43735 -r 8ae418dfe561 src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Sat Sep 17 00:40:27 2011 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Sat Sep 17 15:08:55 2011 +0200
@@ -29,7 +29,7 @@
                              as with < and <= but not = and div*)
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
-  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+  val trans_tac: thm option -> tactic           (*applies the initial lemma*)
   val norm_tac: simpset -> tactic                (*proves the initial lemma*)
   val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
   val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
@@ -72,7 +72,7 @@
   in
     Option.map (export o Data.simplify_meta_eq ss)
       (Data.prove_conv
-         [Data.trans_tac ss reshape, rtac Data.cancel 1,
+         [Data.trans_tac reshape, rtac Data.cancel 1,
           Data.numeral_simp_tac ss] ctxt prems (t', rhs))
   end
   (* FIXME avoid handling of generic exceptions *)
diff -r 64469ea43735 -r 8ae418dfe561 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Sat Sep 17 00:40:27 2011 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Sat Sep 17 15:08:55 2011 +0200
@@ -36,7 +36,7 @@
   val bal_add2: thm
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
-  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+  val trans_tac: thm option -> tactic            (*applies the initial lemma*)
   val norm_tac: simpset -> tactic                (*proves the initial lemma*)
   val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
   val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
@@ -92,12 +92,12 @@
     Option.map (export o Data.simplify_meta_eq ss)
       (if n2 <= n1 then
          Data.prove_conv
-           [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
+           [Data.trans_tac reshape, rtac Data.bal_add1 1,
             Data.numeral_simp_tac ss] ctxt prems
            (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
        else
          Data.prove_conv
-           [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
+           [Data.trans_tac reshape, rtac Data.bal_add2 1,
             Data.numeral_simp_tac ss] ctxt prems
            (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
   end
diff -r 64469ea43735 -r 8ae418dfe561 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Sat Sep 17 00:40:27 2011 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Sat Sep 17 15:08:55 2011 +0200
@@ -29,7 +29,7 @@
   val left_distrib: thm
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> term * term -> thm option
-  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+  val trans_tac: thm option -> tactic            (*applies the initial lemma*)
   val norm_tac: simpset -> tactic                (*proves the initial lemma*)
   val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
   val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
@@ -83,7 +83,7 @@
   in
     Option.map (export o Data.simplify_meta_eq ss)
       (Data.prove_conv
-         [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
+         [Data.trans_tac reshape, rtac Data.left_distrib 1,
           Data.numeral_simp_tac ss] ctxt
          (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
   end
diff -r 64469ea43735 -r 8ae418dfe561 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Sat Sep 17 00:40:27 2011 +0200
+++ b/src/ZF/arith_data.ML	Sat Sep 17 15:08:55 2011 +0200
@@ -165,7 +165,7 @@
   val dest_bal = FOLogic.dest_eq
   val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
   val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
-  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
+  val trans_tac = gen_trans_tac @{thm iff_trans}
   end;
 
 structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
@@ -178,7 +178,7 @@
   val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT
   val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
   val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
-  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
+  val trans_tac = gen_trans_tac @{thm iff_trans}
   end;
 
 structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
@@ -191,7 +191,7 @@
   val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT
   val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
   val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
-  fun trans_tac _ = gen_trans_tac @{thm trans}
+  val trans_tac = gen_trans_tac @{thm trans}
   end;
 
 structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
diff -r 64469ea43735 -r 8ae418dfe561 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Sat Sep 17 00:40:27 2011 +0200
+++ b/src/ZF/int_arith.ML	Sat Sep 17 15:08:55 2011 +0200
@@ -156,7 +156,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val find_first_coeff  = find_first_coeff []
-  fun trans_tac _       = ArithData.gen_trans_tac @{thm iff_trans}
+  val trans_tac         = ArithData.gen_trans_tac @{thm iff_trans}
 
   val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}
   val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
@@ -234,7 +234,7 @@
   val dest_coeff        = dest_coeff 1
   val left_distrib      = @{thm left_zadd_zmult_distrib} RS @{thm trans}
   val prove_conv        = prove_conv_nohyps "int_combine_numerals"
-  fun trans_tac _       = ArithData.gen_trans_tac @{thm trans}
+  val trans_tac         = ArithData.gen_trans_tac @{thm trans}
 
   val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys
   val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
@@ -276,7 +276,7 @@
   fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   val left_distrib      = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
   val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
-  fun trans_tac _       = ArithData.gen_trans_tac @{thm trans}
+  val trans_tac         = ArithData.gen_trans_tac @{thm trans}