diff -r 2e48182cc82c -r cf58b5b794b2 src/HOL/ex/Sqrt_Script.thy
--- a/src/HOL/ex/Sqrt_Script.thy	Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Sqrt_Script.thy	Sat Dec 26 15:59:27 2015 +0100
@@ -52,7 +52,7 @@
 subsection \<open>Main theorem\<close>
 
 text \<open>
-  The square root of any prime number (including @{text 2}) is
+  The square root of any prime number (including \<open>2\<close>) is
   irrational.
 \<close>