diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -170,8 +170,8 @@
 
 text \<open>
 
-To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
-@{const Inf} in theorem names with c.
+To avoid name classes with the \<^class>\<open>complete_lattice\<close>-class we prefix \<^const>\<open>Sup\<close> and
+\<^const>\<open>Inf\<close> in theorem names with c.
 
 \<close>