--- a/src/ZF/Epsilon.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Epsilon.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -48,7 +48,7 @@
 lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD]
 
 lemma Transset_eclose: "Transset(eclose(A))"
-apply (unfold eclose_def Transset_def)
+  unfolding eclose_def Transset_def
 apply (rule subsetI [THEN ballI])
 apply (erule UN_E)
 apply (rule nat_succI [THEN UN_I], assumption)