--- a/src/ZF/Nat.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Nat.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -108,13 +108,13 @@
 lemma Ord_nat [iff]: "Ord(nat)"
 apply (rule OrdI)
 apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset])
-apply (unfold Transset_def)
+  unfolding Transset_def
 apply (rule ballI)
 apply (erule nat_induct, auto)
 done
 
 lemma Limit_nat [iff]: "Limit(nat)"
-apply (unfold Limit_def)
+  unfolding Limit_def
 apply (safe intro!: ltI Ord_nat)
 apply (erule ltD)
 done