--- a/src/ZF/IMP/Equiv.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/IMP/Equiv.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -66,7 +66,7 @@
    apply safe
    apply simp_all
    apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
-   apply (unfold Gamma_def)
+     unfolding Gamma_def
    apply force
   txt \<open>\<open>if\<close>\<close>
   apply auto