diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -671,7 +671,7 @@
       let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
       show ?case
       proof (intro exI conjI)
-        show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>insert F \<F> = Pi\<^sub>E I ?U"
+        show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>(insert F \<F>) = Pi\<^sub>E I ?U"
         using eq  PiE_mem \<open>i \<in> I\<close>  by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
       next
         show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"