src/ZF/func.thy

--- a/src/ZF/func.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/func.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -318,7 +318,7 @@
 by (simp add: restrict_def relation_def, blast)
 
 lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A \<inter> C"
-apply (unfold restrict_def lam_def)
+  unfolding restrict_def lam_def
 apply (rule equalityI)
 apply (auto simp add: domain_iff)
 done