diff -r cb34f5f49a08 -r ec32cdaab97b src/HOL/Algebra/Complete_Lattice.thy
--- a/src/HOL/Algebra/Complete_Lattice.thy	Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Tue Dec 19 13:58:12 2017 +0100
@@ -543,7 +543,7 @@
 end
 
 
-subsection \<open>Complete lattices where @{text eq} is the Equality\<close>
+subsection \<open>Complete lattices where \<open>eq\<close> is the Equality\<close>
 
 locale complete_lattice = partial_order +
   assumes sup_exists: