diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Data_Structures/AA_Set.thy
--- a/src/HOL/Data_Structures/AA_Set.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -72,7 +72,7 @@
                \<Rightarrow> Node (Node l x (lv-1) t2) a (lva+1)
                     (split (Node t3 b (if sngl t1 then lva else lva+1) t4)))))"
 
-text\<open>In the paper, the last case of @{const adjust} is expressed with the help of an
+text\<open>In the paper, the last case of \<^const>\<open>adjust\<close> is expressed with the help of an
 incorrect auxiliary function \texttt{nlvl}.
 
 Function \<open>split_max\<close> below is called \texttt{dellrg} in the paper.