--- a/src/HOL/Integ/int_arith1.ML Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Integ/int_arith1.ML Thu May 11 19:19:31 2006 +0200
@@ -281,8 +281,8 @@
(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
during re-arrangement*)
-val non_add_bin_simps =
- bin_simps \\ [add_number_of_left, number_of_add RS sym];
+val non_add_bin_simps =
+ subtract Thm.eq_thm [add_number_of_left, number_of_add RS sym] bin_simps;
(*To evaluate binary negations of coefficients*)
val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,