diff -r a0e6bda62b7b -r 3d51fbf81c17 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Integ/IntDef.ML	Fri Oct 05 21:52:39 2001 +0200
@@ -7,8 +7,8 @@
 *)
 
 
-(*Rewrite the overloaded 0::int to (int 0)*)
-Addsimps [Zero_def];
+(*Rewrite the overloaded 0::int to (int 0)*)    (* FIXME !? *)
+Addsimps [Zero_int_def];
 
 Goalw  [intrel_def] "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)";
 by (Blast_tac 1);
@@ -326,7 +326,7 @@
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_int0";
 
-Goalw [int_def] "int 1' * z = z";
+Goalw [int_def] "int (Suc 0) * z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_int1";
@@ -335,7 +335,7 @@
 by (rtac ([zmult_commute, zmult_int0] MRS trans) 1);
 qed "zmult_int0_right";
 
-Goal "z * int 1' = z";
+Goal "z * int (Suc 0) = z";
 by (rtac ([zmult_commute, zmult_int1] MRS trans) 1);
 qed "zmult_int1_right";