src/ZF/AC/HH.thy

--- a/src/ZF/AC/HH.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/HH.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -196,7 +196,7 @@
          f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x}\<rbrakk>   
       \<Longrightarrow> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))   
           \<in> bij(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> x})"
-apply (unfold bij_def)
+  unfolding bij_def
 apply (fast intro!: lam_Least_HH_inj lam_surj_sing f_sing_imp_HH_sing)
 done