
diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Nat_Numeral.thy	Tue Sep 06 19:03:41 2011 -0700
@@ -364,7 +364,7 @@
 
 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
 apply (rule sym)
-apply (simp add: nat_eq_iff int_Suc)
+apply (simp add: nat_eq_iff)
 done
 
 lemma Suc_nat_number_of_add:




