diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -1410,7 +1410,7 @@
     ultimately obtain \<C>' where "finite \<C>'" "\<C>' \<subseteq> \<B>'" "U \<subseteq> \<Union>\<C>'"
       using fin [of \<B>'] \<open>topspace X = U\<close> \<open>U \<subseteq> \<Union>\<B>\<close> by blast
     then show ?thesis
-      unfolding \<B>' exists_finite_subset_image \<open>topspace X = U\<close> by auto
+      unfolding \<B>' ex_finite_subset_image \<open>topspace X = U\<close> by auto
   qed
   show ?thesis
     apply (rule Alexander_subbase [where \<B> = "Collect ((\<lambda>x. x \<in> \<B>) relative_to (topspace X))"])