diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Comb.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -86,7 +86,7 @@
 lemma diamond_strip_lemmaD [rule_format]:
   "\<lbrakk>diamond(r);  \<langle>x,y\<rangle>:r^+\<rbrakk> \<Longrightarrow>
     \<forall>y'. <x,y'>:r \<longrightarrow> (\<exists>z. <y',z>: r^+ \<and> \<langle>y,z\<rangle>: r)"
-  apply (unfold diamond_def)
+    unfolding diamond_def
   apply (erule trancl_induct)
    apply (blast intro: r_into_trancl)
   apply clarify
@@ -186,7 +186,7 @@
   by (blast intro: comb_I)
 
 lemma not_diamond_contract: "\<not> diamond(contract)"
-  apply (unfold diamond_def)
+    unfolding diamond_def
   apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3
     elim!: I_contract_E)
   done
@@ -228,7 +228,7 @@
 
 lemma diamond_parcontract: "diamond(parcontract)"
   \<comment> \<open>Church-Rosser property for parallel contraction\<close>
-  apply (unfold diamond_def)
+    unfolding diamond_def
   apply (rule impI [THEN allI, THEN allI])
   apply (erule parcontract.induct)
      apply (blast elim!: comb.free_elims  intro: parcontract_combD2)+