diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -36,7 +36,7 @@
     have sd_pos: "0 < setdist {x} (S - V)" if "V \<in> \<C>" "x \<in> S" "x \<in> V" for V x
     proof -
       have "closedin (subtopology euclidean S) (S - V)"
-        by (simp add: Diff_Diff_Int Diff_subset closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
+        by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
       with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"]
         show ?thesis
           by (simp add: order_class.order.order_iff_strict)