src/ZF/Coind/Map.thy

--- a/src/ZF/Coind/Map.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Coind/Map.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -81,7 +81,7 @@
 
 lemma mapQU:
   "\<lbrakk>m \<in> PMap(A,quniv(B)); \<And>x. x \<in> A \<Longrightarrow> x \<in> univ(B)\<rbrakk> \<Longrightarrow> m \<in> quniv(B)"
-apply (unfold PMap_def TMap_def)
+  unfolding PMap_def TMap_def
 apply (blast intro!: MapQU_lemma [THEN subsetD]) 
 done