--- a/src/HOL/Integ/NatBin.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Integ/NatBin.thy Thu Jan 19 21:22:08 2006 +0100
@@ -591,14 +591,14 @@
val numeral_ss = simpset() addsimps numerals;
val nat_bin_arith_setup =
- [Fast_Arith.map_data
+ Fast_Arith.map_data
(fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
lessD = lessD, neqE = neqE,
simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
not_neg_number_of_Pls,
- neg_number_of_Min,neg_number_of_BIT]})]
+ neg_number_of_Min,neg_number_of_BIT]})
*}
setup nat_bin_arith_setup