diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -1763,7 +1763,7 @@
     by auto
   moreover
   have ev_Z: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> z) F"
-    unfolding Z_def by (auto elim: eventually_mono intro: set_mp[OF closure_subset])
+    unfolding Z_def by (auto elim: eventually_mono intro: subsetD[OF closure_subset])
   have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
   proof (intro allI impI)
     fix B assume "finite B" "B \<subseteq> Z"