--- a/src/HOL/Tools/string_syntax.ML Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML Thu Feb 11 23:00:22 2010 +0100
@@ -30,7 +30,7 @@
fun mk_char s =
if Symbol.is_ascii s then
- Syntax.Appl [Syntax.Constant "Char", mk_nib (ord s div 16), mk_nib (ord s mod 16)]
+ Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
else error ("Non-ASCII symbol: " ^ quote s);
val specials = explode "\\\"`'";
@@ -41,11 +41,13 @@
then c else raise Match
end;
-fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
+fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
| dest_char _ = raise Match;
fun syntax_string cs =
- Syntax.Appl [Syntax.Constant "_inner_string", Syntax.Variable (Syntax.implode_xstr cs)];
+ Syntax.Appl
+ [Syntax.Constant @{syntax_const "_inner_string"},
+ Syntax.Variable (Syntax.implode_xstr cs)];
fun char_ast_tr [Syntax.Variable xstr] =
@@ -54,24 +56,29 @@
| _ => error ("Single character expected: " ^ xstr))
| char_ast_tr asts = raise AST ("char_ast_tr", asts);
-fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_string [dest_chr c1 c2]]
+fun char_ast_tr' [c1, c2] =
+ Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
| char_ast_tr' _ = raise Match;
(* string *)
-fun mk_string [] = Syntax.Constant "Nil"
- | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
+fun mk_string [] = Syntax.Constant @{const_syntax Nil}
+ | mk_string (c :: cs) =
+ Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
fun string_ast_tr [Syntax.Variable xstr] =
(case Syntax.explode_xstr xstr of
- [] => Syntax.Appl
- [Syntax.Constant Syntax.constrainC, Syntax.Constant "Nil", Syntax.Constant "string"]
+ [] =>
+ Syntax.Appl
+ [Syntax.Constant Syntax.constrainC,
+ Syntax.Constant @{const_syntax Nil}, Syntax.Constant "string"] (* FIXME @{type_syntax} *)
| cs => mk_string cs)
| string_ast_tr asts = raise AST ("string_tr", asts);
-fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
- syntax_string (map dest_char (Syntax.unfold_ast "_args" args))]
+fun list_ast_tr' [args] =
+ Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
+ syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
| list_ast_tr' ts = raise Match;
@@ -79,7 +86,7 @@
val setup =
Sign.add_trfuns
- ([("_Char", char_ast_tr), ("_String", string_ast_tr)], [], [],
- [("Char", char_ast_tr'), ("@list", list_ast_tr')]);
+ ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
+ [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
end;