diff -r 8300bba275e3 -r b98365c6e869 src/Pure/Thy/thy_parse.ML
--- 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\