diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -374,7 +374,7 @@
 
 subsection "Insertion Sort w.r.t. Keys and Stability"
 
-text \<open>Note that @{const insort_key} is already defined in theory @{theory HOL.List}.
+text \<open>Note that \<^const>\<open>insort_key\<close> is already defined in theory \<^theory>\<open>HOL.List\<close>.
 Thus some of the lemmas are already present as well.\<close>
 
 fun isort_key :: "('a \<Rightarrow> 'k::linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list" where