src/HOL/Library/Numeral_Type.thy

--- a/src/HOL/Library/Numeral_Type.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -182,7 +182,7 @@
 subsection \<open>Ring class instances\<close>
 
 text \<open>
-  Unfortunately @{text ring_1} instance is not possible for
+  Unfortunately \<open>ring_1\<close> instance is not possible for
   @{typ num1}, since 0 and 1 are not distinct.
 \<close>