src/Pure/Thy/thy_parse.ML
changeset 2694 b98365c6e869
parent 2385 73d1435aa729
child 3110 dfc1d659f968
--- a/src/Pure/Thy/thy_parse.ML	Fri Feb 28 16:39:30 1997 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Fri Feb 28 16:40:08 1997 +0100
@@ -338,7 +338,8 @@
   \ val parse_translation = [];\n\
   \ val print_translation = [];\n\
   \ val typed_print_translation = [];\n\
-  \ val print_ast_translation = [];";
+  \ val print_ast_translation = [];\n\
+  \ val token_translation = [];";
 
 val trfun_args =
   "(parse_ast_translation, parse_translation, \
@@ -482,6 +483,7 @@
         \|> add_trfuns\n"
         ^ trfun_args ^ "\n\
         \|> add_trfunsT typed_print_translation \n\
+        \|> add_tokentrfuns token_translation \n\
         \\n"
         ^ extxt ^ "\n\
         \\n\