--- a/src/HOL/String.thy Tue Feb 14 22:48:07 2012 +0100
+++ b/src/HOL/String.thy Wed Feb 15 13:24:22 2012 +0100
@@ -69,7 +69,7 @@
by (simp add: fun_eq_iff split: char.split)
syntax
- "_Char" :: "xstr_position => char" ("CHR _")
+ "_Char" :: "str_position => char" ("CHR _")
subsection {* Strings *}
@@ -77,7 +77,7 @@
type_synonym string = "char list"
syntax
- "_String" :: "xstr_position => string" ("_")
+ "_String" :: "str_position => string" ("_")
use "Tools/string_syntax.ML"
setup String_Syntax.setup