diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -2792,7 +2792,7 @@
     show "U ` \<F> \<subseteq> \<U>"
       using \<open>\<F> \<subseteq> \<V>\<close> U by auto
   next
-    show "f ` S \<subseteq> UNION \<F> U"
+    show "f ` S \<subseteq> \<Union> (U ` \<F>)"
       using \<F>(2-3) U UnionE subset_eq U by fastforce
   qed
 qed