src/Pure/Thy/thy_parse.ML
changeset 4047 67b5552b1067
parent 4020 f88775cc8d17
child 4056 abb0f4742ed7
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Thu Oct 30 16:59:56 1997 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Thu Oct 30 17:00:34 1997 +0100
     1.3 @@ -341,13 +341,14 @@
     1.4  
     1.5  (* ML translations *)
     1.6  
     1.7 -val trfun_defs =
     1.8 +val local_defs =
     1.9    " val parse_ast_translation = [];\n\
    1.10    \ val parse_translation = [];\n\
    1.11    \ val print_translation = [];\n\
    1.12    \ val typed_print_translation = [];\n\
    1.13    \ val print_ast_translation = [];\n\
    1.14 -  \ val token_translation = [];";
    1.15 +  \ val token_translation = [];\n\
    1.16 +  \ val thy_data = []";
    1.17  
    1.18  val trfun_args =
    1.19    "(parse_ast_translation, parse_translation, \
    1.20 @@ -490,7 +491,7 @@
    1.21      \\n\
    1.22      \local\n\
    1.23      \ val thy_name = \"" ^ tname ^ "\";\n"
    1.24 -    ^ trfun_defs ^ "\n\
    1.25 +    ^ local_defs ^ "\n\
    1.26      \in\n\
    1.27      \\n"
    1.28      ^ mltxt ^ "\n\
    1.29 @@ -501,8 +502,9 @@
    1.30      "\n\
    1.31      \|> Theory.add_trfuns\n"
    1.32      ^ trfun_args ^ "\n\
    1.33 -    \|> Theory.add_trfunsT typed_print_translation \n\
    1.34 -    \|> Theory.add_tokentrfuns token_translation \n\
    1.35 +    \|> Theory.add_trfunsT typed_print_translation\n\
    1.36 +    \|> Theory.add_tokentrfuns token_translation\n\
    1.37 +    \|> Theory.init_data thy_data\n\
    1.38      \\n"
    1.39      ^ extxt ^ "\n\
    1.40      \\n\