src/HOL/Integ/int_arith1.ML

--- a/src/HOL/Integ/int_arith1.ML	Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Mon Oct 08 15:23:20 2001 +0200
@@ -410,7 +410,7 @@
 		 zmult_1, zmult_1_right, 
 		 zmult_minus1, zmult_minus1_right,
 		 zminus_zadd_distrib, zminus_zminus, zmult_assoc,
-                 Zero_int_def, int_0, zadd_int RS sym, int_Suc];
+                 Zero_int_def, One_int_def, int_0, int_1, zadd_int RS sym, int_Suc];
 
 val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
                Int_Numeral_Simprocs.cancel_numerals;