diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Complete_Partial_Order.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -11,7 +11,7 @@
 
 subsection \<open>Monotone functions\<close>
 
-text \<open>Dictionary-passing version of @{const Orderings.mono}.\<close>
+text \<open>Dictionary-passing version of \<^const>\<open>Orderings.mono\<close>.\<close>
 
 definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"