src/ZF/Induct/Tree_Forest.thy

--- a/src/ZF/Induct/Tree_Forest.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -109,7 +109,7 @@
 \<rbrakk> \<Longrightarrow> (\<forall>t \<in> tree(A).    tree_forest_rec(b,c,d,t) \<in> C(t)) \<and>
           (\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
     \<comment> \<open>Mutually recursive version.\<close>
-  apply (unfold Ball_def)
+    unfolding Ball_def
   apply (rule tree_forest.mutual_induct)
   apply simp_all
   done