diff -r bb5eda7416e5 -r d49ffd9f9662 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Tue Feb 18 19:13:47 2003 +0100
+++ b/src/ZF/Nat.thy	Wed Feb 19 10:53:27 2003 +0100
@@ -113,11 +113,11 @@
 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
 by (induct a rule: nat_induct, auto)
 
-lemma succ_natD [dest!]: "succ(i): nat ==> i: nat"
+lemma succ_natD: "succ(i): nat ==> i: nat"
 by (rule Ord_trans [OF succI1], auto)
 
 lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
-by blast
+by (blast dest!: succ_natD)
 
 lemma nat_le_Limit: "Limit(i) ==> nat le i"
 apply (rule subset_imp_le)