src/HOL/ex/PER.thy

--- a/src/HOL/ex/PER.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/ex/PER.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -149,7 +149,7 @@
 
 text \<open>
   The quotient type \<open>'a quot\<close> consists of all
-  \emph{equivalence classes} over elements of the base type @{typ 'a}.
+  \emph{equivalence classes} over elements of the base type \<^typ>\<open>'a\<close>.
 \<close>
 
 definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"