diff -r d2c19aea17bc -r 8c43ffe2bb32 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Mon Sep 06 17:37:35 2004 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Tue Sep 07 11:42:50 2004 +0200
@@ -524,7 +524,7 @@
                       addcongs [if_weak_cong]}),
   arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT),
   arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT),
-  arith_discrete ("IntDef.int", true)];
+  arith_discrete "IntDef.int"];
 
 end;