src/HOL/Nitpick.thy

--- a/src/HOL/Nitpick.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Nitpick.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -116,7 +116,7 @@
 
 text \<open>
 Auxiliary definitions used to provide an alternative representation for
-@{text rat} and @{text real}.
+\<open>rat\<close> and \<open>real\<close>.
 \<close>
 
 function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where