diff -r d2be0579a2c8 -r 1fe0ec14a90a src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Dec 21 18:11:24 2017 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Dec 21 19:09:18 2017 +0100
@@ -8262,10 +8262,10 @@
       by (meson Topological_Spaces.connected_continuous_image \<open>connected S\<close> homeomorphism_cont1 homeomorphism_of_subsets homhj hull_subset top_greatest)
     have hUS: "h ` U \<subseteq> h ` S"
       by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq)
-    have op: "openin (subtopology euclidean (affine hull S)) U \<Longrightarrow> open (h ` U)" for U
+    have opn: "openin (subtopology euclidean (affine hull S)) U \<Longrightarrow> open (h ` U)" for U
       using homeomorphism_imp_open_map [OF homhj]  by simp
     have "open (h ` U)" "open (h ` S)"
-      by (auto intro: opeS opeU openin_trans op)
+      by (auto intro: opeS opeU openin_trans opn)
     then obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g"
                  and f: "\<And>x. x \<in> h ` K \<Longrightarrow> f x \<in> h ` U"
                  and sub: "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> h ` S"