# HG changeset patch
# User nipkow
# Date 977413930 -3600
# Node ID 8666477dd9a2bf7edc722f24d6417554a2218ed1
# Parent  c058f78c354479e2850df2dfe9a5e4946f59a8d5
*** empty log message ***

diff -r c058f78c3544 -r 8666477dd9a2 src/HOL/Integ/int_arith1.ML
--- 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;