dropped unused argument – avoids problem with SML/NJ
authorhaftmann
Sat Sep 17 15:08:55 2011 +0200 (2011-09-17)
changeset 449478ae418dfe561
parent 44946 64469ea43735
child 44948 b455e4f42c04
dropped unused argument – avoids problem with SML/NJ
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral_simprocs.ML
src/Provers/Arith/cancel_numeral_factor.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
src/ZF/arith_data.ML
src/ZF/int_arith.ML
     1.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Sep 17 00:40:27 2011 +0200
     1.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Sep 17 15:08:55 2011 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4    val mk_coeff = mk_coeff
     1.5    val dest_coeff = dest_coeff
     1.6    val find_first_coeff = find_first_coeff []
     1.7 -  val trans_tac = K Numeral_Simprocs.trans_tac
     1.8 +  val trans_tac = Numeral_Simprocs.trans_tac
     1.9  
    1.10    val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.11      [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
    1.12 @@ -233,7 +233,7 @@
    1.13    val dest_coeff = dest_coeff
    1.14    val left_distrib = @{thm left_add_mult_distrib} RS trans
    1.15    val prove_conv = Arith_Data.prove_conv_nohyps
    1.16 -  val trans_tac = K Numeral_Simprocs.trans_tac
    1.17 +  val trans_tac = Numeral_Simprocs.trans_tac
    1.18  
    1.19    val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac}
    1.20    val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.21 @@ -259,7 +259,7 @@
    1.22  struct
    1.23    val mk_coeff = mk_coeff
    1.24    val dest_coeff = dest_coeff
    1.25 -  val trans_tac = K Numeral_Simprocs.trans_tac
    1.26 +  val trans_tac = Numeral_Simprocs.trans_tac
    1.27  
    1.28    val norm_ss1 = Numeral_Simprocs.num_ss addsimps
    1.29      numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
    1.30 @@ -361,7 +361,7 @@
    1.31    val mk_coeff = mk_coeff
    1.32    val dest_coeff = dest_coeff
    1.33    val find_first = find_first_t []
    1.34 -  val trans_tac = K Numeral_Simprocs.trans_tac
    1.35 +  val trans_tac = Numeral_Simprocs.trans_tac
    1.36    val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
    1.37    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
    1.38    val simplify_meta_eq  = cancel_simplify_meta_eq
     2.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sat Sep 17 00:40:27 2011 +0200
     2.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Sep 17 15:08:55 2011 +0200
     2.3 @@ -214,7 +214,7 @@
     2.4    val mk_coeff = mk_coeff
     2.5    val dest_coeff = dest_coeff 1
     2.6    val find_first_coeff = find_first_coeff []
     2.7 -  val trans_tac = K trans_tac
     2.8 +  val trans_tac = trans_tac
     2.9  
    2.10    fun norm_tac ss =
    2.11      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    2.12 @@ -289,7 +289,7 @@
    2.13    val dest_coeff = dest_coeff 1
    2.14    val left_distrib = @{thm combine_common_factor} RS trans
    2.15    val prove_conv = Arith_Data.prove_conv_nohyps
    2.16 -  val trans_tac = K trans_tac
    2.17 +  val trans_tac = trans_tac
    2.18  
    2.19    fun norm_tac ss =
    2.20      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    2.21 @@ -315,7 +315,7 @@
    2.22    val dest_coeff = dest_fcoeff 1
    2.23    val left_distrib = @{thm combine_common_factor} RS trans
    2.24    val prove_conv = Arith_Data.prove_conv_nohyps
    2.25 -  val trans_tac = K trans_tac
    2.26 +  val trans_tac = trans_tac
    2.27  
    2.28    val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
    2.29    fun norm_tac ss =
    2.30 @@ -365,7 +365,7 @@
    2.31  struct
    2.32    val mk_coeff = mk_coeff
    2.33    val dest_coeff = dest_coeff 1
    2.34 -  val trans_tac = K trans_tac
    2.35 +  val trans_tac = trans_tac
    2.36  
    2.37    val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
    2.38    val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
    2.39 @@ -507,7 +507,7 @@
    2.40    val mk_coeff = mk_coeff
    2.41    val dest_coeff = dest_coeff
    2.42    val find_first = find_first_t []
    2.43 -  val trans_tac = K trans_tac
    2.44 +  val trans_tac = trans_tac
    2.45    val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
    2.46    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
    2.47    val simplify_meta_eq  = cancel_simplify_meta_eq 
     3.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML	Sat Sep 17 00:40:27 2011 +0200
     3.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML	Sat Sep 17 15:08:55 2011 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4                               as with < and <= but not = and div*)
     3.5    (*proof tools*)
     3.6    val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
     3.7 -  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
     3.8 +  val trans_tac: thm option -> tactic           (*applies the initial lemma*)
     3.9    val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    3.10    val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
    3.11    val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
    3.12 @@ -72,7 +72,7 @@
    3.13    in
    3.14      Option.map (export o Data.simplify_meta_eq ss)
    3.15        (Data.prove_conv
    3.16 -         [Data.trans_tac ss reshape, rtac Data.cancel 1,
    3.17 +         [Data.trans_tac reshape, rtac Data.cancel 1,
    3.18            Data.numeral_simp_tac ss] ctxt prems (t', rhs))
    3.19    end
    3.20    (* FIXME avoid handling of generic exceptions *)
     4.1 --- a/src/Provers/Arith/cancel_numerals.ML	Sat Sep 17 00:40:27 2011 +0200
     4.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Sat Sep 17 15:08:55 2011 +0200
     4.3 @@ -36,7 +36,7 @@
     4.4    val bal_add2: thm
     4.5    (*proof tools*)
     4.6    val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
     4.7 -  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
     4.8 +  val trans_tac: thm option -> tactic            (*applies the initial lemma*)
     4.9    val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    4.10    val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
    4.11    val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
    4.12 @@ -92,12 +92,12 @@
    4.13      Option.map (export o Data.simplify_meta_eq ss)
    4.14        (if n2 <= n1 then
    4.15           Data.prove_conv
    4.16 -           [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
    4.17 +           [Data.trans_tac reshape, rtac Data.bal_add1 1,
    4.18              Data.numeral_simp_tac ss] ctxt prems
    4.19             (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
    4.20         else
    4.21           Data.prove_conv
    4.22 -           [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
    4.23 +           [Data.trans_tac reshape, rtac Data.bal_add2 1,
    4.24              Data.numeral_simp_tac ss] ctxt prems
    4.25             (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
    4.26    end
     5.1 --- a/src/Provers/Arith/combine_numerals.ML	Sat Sep 17 00:40:27 2011 +0200
     5.2 +++ b/src/Provers/Arith/combine_numerals.ML	Sat Sep 17 15:08:55 2011 +0200
     5.3 @@ -29,7 +29,7 @@
     5.4    val left_distrib: thm
     5.5    (*proof tools*)
     5.6    val prove_conv: tactic list -> Proof.context -> term * term -> thm option
     5.7 -  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
     5.8 +  val trans_tac: thm option -> tactic            (*applies the initial lemma*)
     5.9    val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    5.10    val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
    5.11    val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
    5.12 @@ -83,7 +83,7 @@
    5.13    in
    5.14      Option.map (export o Data.simplify_meta_eq ss)
    5.15        (Data.prove_conv
    5.16 -         [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
    5.17 +         [Data.trans_tac reshape, rtac Data.left_distrib 1,
    5.18            Data.numeral_simp_tac ss] ctxt
    5.19           (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    5.20    end
     6.1 --- a/src/ZF/arith_data.ML	Sat Sep 17 00:40:27 2011 +0200
     6.2 +++ b/src/ZF/arith_data.ML	Sat Sep 17 15:08:55 2011 +0200
     6.3 @@ -165,7 +165,7 @@
     6.4    val dest_bal = FOLogic.dest_eq
     6.5    val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
     6.6    val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
     6.7 -  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
     6.8 +  val trans_tac = gen_trans_tac @{thm iff_trans}
     6.9    end;
    6.10  
    6.11  structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
    6.12 @@ -178,7 +178,7 @@
    6.13    val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT
    6.14    val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
    6.15    val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
    6.16 -  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
    6.17 +  val trans_tac = gen_trans_tac @{thm iff_trans}
    6.18    end;
    6.19  
    6.20  structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
    6.21 @@ -191,7 +191,7 @@
    6.22    val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT
    6.23    val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
    6.24    val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
    6.25 -  fun trans_tac _ = gen_trans_tac @{thm trans}
    6.26 +  val trans_tac = gen_trans_tac @{thm trans}
    6.27    end;
    6.28  
    6.29  structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
     7.1 --- a/src/ZF/int_arith.ML	Sat Sep 17 00:40:27 2011 +0200
     7.2 +++ b/src/ZF/int_arith.ML	Sat Sep 17 15:08:55 2011 +0200
     7.3 @@ -156,7 +156,7 @@
     7.4    val mk_coeff          = mk_coeff
     7.5    val dest_coeff        = dest_coeff 1
     7.6    val find_first_coeff  = find_first_coeff []
     7.7 -  fun trans_tac _       = ArithData.gen_trans_tac @{thm iff_trans}
     7.8 +  val trans_tac         = ArithData.gen_trans_tac @{thm iff_trans}
     7.9  
    7.10    val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}
    7.11    val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
    7.12 @@ -234,7 +234,7 @@
    7.13    val dest_coeff        = dest_coeff 1
    7.14    val left_distrib      = @{thm left_zadd_zmult_distrib} RS @{thm trans}
    7.15    val prove_conv        = prove_conv_nohyps "int_combine_numerals"
    7.16 -  fun trans_tac _       = ArithData.gen_trans_tac @{thm trans}
    7.17 +  val trans_tac         = ArithData.gen_trans_tac @{thm trans}
    7.18  
    7.19    val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys
    7.20    val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
    7.21 @@ -276,7 +276,7 @@
    7.22    fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
    7.23    val left_distrib      = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
    7.24    val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
    7.25 -  fun trans_tac _       = ArithData.gen_trans_tac @{thm trans}
    7.26 +  val trans_tac         = ArithData.gen_trans_tac @{thm trans}
    7.27  
    7.28  
    7.29