src/HOL/Algebra/Congruence.thy

--- a/src/HOL/Algebra/Congruence.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Algebra/Congruence.thy	Thu May 26 17:51:22 2016 +0200
@@ -15,7 +15,7 @@
   carrier :: "'a set"
 
 
-subsection \<open>Structure with Carrier and Equivalence Relation @{text eq}\<close>
+subsection \<open>Structure with Carrier and Equivalence Relation \<open>eq\<close>\<close>
 
 record 'a eq_object = "'a partial_object" +
   eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)