--- 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>