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: