--- a/src/HOL/Analysis/Path_Connected.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Tue Jan 17 13:59:10 2017 +0100
@@ -7099,7 +7099,7 @@
subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
-subsubsection\<open>The theorem @{text homeomorphism_moving_points_exists}\<close>
+subsubsection\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
lemma homeomorphism_moving_point_1:
fixes a :: "'a::euclidean_space"
@@ -7521,7 +7521,7 @@
qed
-subsubsection\<open>The theorem @{text homeomorphism_grouping_points_exists}\<close>
+subsubsection\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
lemma homeomorphism_grouping_point_1:
fixes a::real and c::real