src/HOL/String.thy
changeset 45490 20c8c0cca555
parent 45182 10202ca034b0
child 46483 10a9c31a22b4
     1.1 --- a/src/HOL/String.thy	Mon Nov 14 17:47:59 2011 +0100
     1.2 +++ b/src/HOL/String.thy	Mon Nov 14 17:48:26 2011 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4    by (simp add: fun_eq_iff split: char.split)
     1.5  
     1.6  syntax
     1.7 -  "_Char" :: "xstr => char"    ("CHR _")
     1.8 +  "_Char" :: "xstr_position => char"    ("CHR _")
     1.9  
    1.10  
    1.11  subsection {* Strings *}
    1.12 @@ -77,7 +77,7 @@
    1.13  type_synonym string = "char list"
    1.14  
    1.15  syntax
    1.16 -  "_String" :: "xstr => string"    ("_")
    1.17 +  "_String" :: "xstr_position => string"    ("_")
    1.18  
    1.19  use "Tools/string_syntax.ML"
    1.20  setup String_Syntax.setup