diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -633,7 +633,7 @@
   shows "t_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
 using assms t_get_min_rest_bound_aux unfolding invar_def by blast
 
-text\<open>Note that although the definition of function @{const rev} has quadratic complexity,
+text\<open>Note that although the definition of function \<^const>\<open>rev\<close> has quadratic complexity,
 it can and is implemented (via suitable code lemmas) as a linear time function.
 Thus the following definition is justified:\<close>