src/ZF/Coind/ECR.thy

--- a/src/ZF/Coind/ECR.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Coind/ECR.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -98,7 +98,7 @@
       v_clos(x,e,ve_owr(ve,f,cl)) = cl;                           
       hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel\<rbrakk> \<Longrightarrow>        
    \<langle>cl,t\<rangle> \<in> HasTyRel"
-apply (unfold hastyenv_def)
+  unfolding hastyenv_def
 apply (erule elab_fixE, safe)
 apply hypsubst_thin
 apply (rule subst, assumption)