--- a/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 02 14:43:47 2009 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 02 16:52:37 2009 +0200
@@ -149,7 +149,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first_coeff = find_first_coeff []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
[@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -238,7 +238,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 Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
@@ -263,7 +263,7 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps
numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -369,7 +369,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first_t []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.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
@@ -380,7 +380,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
);
structure LessCancelFactor = ExtractCommonTermFun
@@ -388,7 +388,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
);
structure LeCancelFactor = ExtractCommonTermFun
@@ -396,7 +396,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
);
structure DivideCancelFactor = ExtractCommonTermFun
@@ -404,7 +404,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
);
structure DvdCancelFactor = ExtractCommonTermFun
@@ -412,7 +412,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
);
val cancel_factor =