diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/integ.ML
--- a/src/ZF/ex/integ.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/integ.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -185,7 +185,7 @@
     "n: nat ==> znegative($~ $# succ(n))";
 by (simp_tac (intrel_ss addsimps [zminus,nnat]) 1);
 by (REPEAT 
-    (resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
+    (resolve_tac [refl, exI, conjI, nat_0_in_succ,
 		  refl RS intrelI RS imageI, consI1, nnat, nat_0I,
 		  nat_succI] 1));
 val znegative_zminus_znat = result();
@@ -377,7 +377,7 @@
 by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
 val zmult_0 = result();
 
-goalw Integ.thy [integ_def,znat_def,one_def]
+goalw Integ.thy [integ_def,znat_def]
     "!!z. z : integ ==> $#1 $* z = z";
 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
 by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1);