src/HOL/Tools/string_syntax.ML

--- a/src/HOL/Tools/string_syntax.ML	Mon Jan 20 20:38:51 2014 +0100
+++ b/src/HOL/Tools/string_syntax.ML	Wed Jan 22 15:10:33 2014 +0100
@@ -38,24 +38,24 @@
 val specials = raw_explode "\\\"`'";
 
 fun dest_chr c1 c2 =
-  let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
-    if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
-    then c
-    else if c = "\n" then "\<newline>"
+  let val s = chr (dest_nib c1 * 16 + dest_nib c2) in
+    if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
+    then s
+    else if s = "\n" then "\<newline>"
     else raise Match
   end;
 
 fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
   | dest_char _ = raise Match;
 
-fun syntax_string cs =
+fun syntax_string ss =
   Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
-    Ast.Variable (Lexicon.implode_str cs)];
+    Ast.Variable (Lexicon.implode_str ss)];
 
 
 fun char_ast_tr [Ast.Variable str] =
-      (case Lexicon.explode_str str of
-        [c] => mk_char c
+      (case Lexicon.explode_str (str, Position.none) of
+        [(s, _)] => mk_char s
       | _ => error ("Single character expected: " ^ str))
   | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
       Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
@@ -69,16 +69,16 @@
 (* string *)
 
 fun mk_string [] = Ast.Constant @{const_syntax Nil}
-  | mk_string (c :: cs) =
-      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
+  | mk_string (s :: ss) =
+      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char s, mk_string ss];
 
 fun string_ast_tr [Ast.Variable str] =
-      (case Lexicon.explode_str str of
+      (case Lexicon.explode_str (str, Position.none) of
         [] =>
           Ast.Appl
             [Ast.Constant @{syntax_const "_constrain"},
               Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
-      | cs => mk_string cs)
+      | ss => mk_string (map Symbol_Pos.symbol ss))
   | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
       Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
   | string_ast_tr asts = raise Ast.AST ("string_tr", asts);