src/Pure/Thy/thy_parse.ML
changeset 2694 b98365c6e869
parent 2385 73d1435aa729
child 3110 dfc1d659f968
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Feb 28 16:39:30 1997 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Feb 28 16:40:08 1997 +0100
     1.3 @@ -338,7 +338,8 @@
     1.4    \ val parse_translation = [];\n\
     1.5    \ val print_translation = [];\n\
     1.6    \ val typed_print_translation = [];\n\
     1.7 -  \ val print_ast_translation = [];";
     1.8 +  \ val print_ast_translation = [];\n\
     1.9 +  \ val token_translation = [];";
    1.10  
    1.11  val trfun_args =
    1.12    "(parse_ast_translation, parse_translation, \
    1.13 @@ -482,6 +483,7 @@
    1.14          \|> add_trfuns\n"
    1.15          ^ trfun_args ^ "\n\
    1.16          \|> add_trfunsT typed_print_translation \n\
    1.17 +        \|> add_tokentrfuns token_translation \n\
    1.18          \\n"
    1.19          ^ extxt ^ "\n\
    1.20          \\n\