diff -r 412fe0623c5d -r ad4b8b6892c3 src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Apr 24 22:22:25 2018 +0100
+++ b/src/HOL/String.thy	Wed Apr 25 09:04:25 2018 +0000
@@ -119,7 +119,7 @@
 lemma char_of_nat [simp]:
   "char_of (of_nat n) = char_of n"
   by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
-	
+
 end
 
 lemma inj_on_char_of_nat [simp]:
@@ -407,7 +407,7 @@
 
   \<^enum> Printable text as string prefixed with @{text STR};
 
-  \<^enum> A single ascii value as numerical value prefixed with @{text ASCII}.
+  \<^enum> A single ascii value as numerical hexadecimal value prefixed with @{text STR}.
 \<close>
 
 instantiation String.literal :: zero
@@ -455,8 +455,8 @@
 code_datatype "0 :: String.literal" String.Literal
 
 syntax
-  "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("ASCII _")
   "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
+  "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
 
 ML_file "Tools/literal.ML"