--- a/src/HOL/Integ/int_arith1.ML Thu Dec 21 16:19:39 2000 +0100
+++ b/src/HOL/Integ/int_arith1.ML Thu Dec 21 16:52:10 2000 +0100
@@ -409,8 +409,8 @@
zmult_0, zmult_0_right,
zmult_1, zmult_1_right,
zmult_minus1, zmult_minus1_right,
- zminus_zadd_distrib, zminus_zminus,
- int_0, zadd_int RS sym, int_Suc];
+ zminus_zadd_distrib, zminus_zminus, zmult_assoc,
+ IntDef.Zero_def, int_0, zadd_int RS sym, int_Suc];
val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
Int_Numeral_Simprocs.cancel_numerals;