1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue May 06 12:51:23 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue May 06 12:55:07 1997 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4    | ident_no_colon _ ((k, s, n) :: _) =
     1.5        syn_err (name_of_kind Ident) (quote s) n;
     1.6  
     1.7 -(*Type used in types, consts and syntax sections*)
     1.8 +(*type used in types, consts and syntax sections*)
     1.9  fun const_type allow_comma toks =
    1.10    let val simple_type =
    1.11          (ident ||
    1.12 @@ -345,16 +345,6 @@
    1.13    "(parse_ast_translation, parse_translation, \
    1.14    \print_translation, print_ast_translation)";
    1.15  
    1.16 -fun mk_mltrans txt =
    1.17 -  "let\n"
    1.18 -  ^ trfun_defs ^ "\n"
    1.19 -  ^ txt ^ "\n\
    1.20 -  \in\n\
    1.21 -  \ " ^ trfun_args ^ "\n\
    1.22 -  \end";
    1.23 -
    1.24 -val mltrans = verbatim >> mk_mltrans;
    1.25 -
    1.26  
    1.27  (* axioms *)
    1.28  
    1.29 @@ -551,8 +541,6 @@
    1.30    section "consts" "|> add_consts" const_decls,
    1.31    section "syntax" "|> add_modesyntax" syntax_decls,
    1.32    section "translations" "|> add_trrules" trans_decls,
    1.33 -  section "MLtrans" "|> add_trfuns" mltrans,
    1.34 -  section "MLtext" "" verbatim,
    1.35    axm_section "rules" "|> add_axioms" axiom_decls,
    1.36    axm_section "defs" "|> add_defs" axiom_decls,
    1.37    axm_section "constdefs" "|> add_consts" constaxiom_decls,