# HG changeset patch
# User wenzelm
# Date 862916107 -7200
# Node ID dfc1d659f9680ea056001a00c0380b3e5874fe88
# Parent  d95748813188a06b039a7780961c1a6ab658e783
removed MLtrans, MLtext;

diff -r d95748813188 -r dfc1d659f968 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue May 06 12:51:23 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Tue May 06 12:55:07 1997 +0200
@@ -244,7 +244,7 @@
   | ident_no_colon _ ((k, s, n) :: _) =
       syn_err (name_of_kind Ident) (quote s) n;
 
-(*Type used in types, consts and syntax sections*)
+(*type used in types, consts and syntax sections*)
 fun const_type allow_comma toks =
   let val simple_type =
         (ident ||
@@ -345,16 +345,6 @@
   "(parse_ast_translation, parse_translation, \
   \print_translation, print_ast_translation)";
 
-fun mk_mltrans txt =
-  "let\n"
-  ^ trfun_defs ^ "\n"
-  ^ txt ^ "\n\
-  \in\n\
-  \ " ^ trfun_args ^ "\n\
-  \end";
-
-val mltrans = verbatim >> mk_mltrans;
-
 
 (* axioms *)
 
@@ -551,8 +541,6 @@
   section "consts" "|> add_consts" const_decls,
   section "syntax" "|> add_modesyntax" syntax_decls,
   section "translations" "|> add_trrules" trans_decls,
-  section "MLtrans" "|> add_trfuns" mltrans,
-  section "MLtext" "" verbatim,
   axm_section "rules" "|> add_axioms" axiom_decls,
   axm_section "defs" "|> add_defs" axiom_decls,
   axm_section "constdefs" "|> add_consts" constaxiom_decls,