--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 22 12:00:16 2019 +0000
@@ -154,7 +154,7 @@
proof
assume ?lhs
then have "0 < r'"
- by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less set_mp)
+ by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less subsetD)
then have "(cball a r \<subseteq> cball a' r')"
by (metis False\<open>?lhs\<close> closure_ball closure_mono not_less)
then show ?rhs