--- 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}