diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -69,7 +69,7 @@
 
 lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
 
-text\<open>Splay trees need two additional @{const ins_list} lemmas:\<close>
+text\<open>Splay trees need two additional \<^const>\<open>ins_list\<close> lemmas:\<close>
 
 lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs"
 by (induction xs) auto
@@ -135,7 +135,7 @@
   del_list_sorted4
   del_list_sorted5
 
-text\<open>Splay trees need two additional @{const del_list} lemmas:\<close>
+text\<open>Splay trees need two additional \<^const>\<open>del_list\<close> lemmas:\<close>
 
 lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs"
 by(induction xs)(fastforce simp: sorted_Cons_iff)+