--- a/src/HOL/Tools/string_syntax.ML Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Tools/string_syntax.ML Sat May 25 15:37:53 2013 +0200
@@ -87,8 +87,11 @@
(* theory setup *)
val setup =
- Sign.add_trfuns
- ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
- [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
+ Sign.parse_ast_translation
+ [(@{syntax_const "_Char"}, K char_ast_tr),
+ (@{syntax_const "_String"}, K string_ast_tr)] #>
+ Sign.print_ast_translation
+ [(@{const_syntax Char}, K char_ast_tr'),
+ (@{syntax_const "_list"}, K list_ast_tr')];
end;