--- a/src/ZF/Sum.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Sum.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -29,7 +29,7 @@
 
 lemma Part_iff:
     "a \<in> Part(A,h) \<longleftrightarrow> a \<in> A \<and> (\<exists>y. a=h(y))"
-apply (unfold Part_def)
+  unfolding Part_def
 apply (rule separation)
 done
 
@@ -46,7 +46,7 @@
 done
 
 lemma Part_subset: "Part(A,h) \<subseteq> A"
-apply (unfold Part_def)
+  unfolding Part_def
 apply (rule Collect_subset)
 done