1.1 --- a/src/Pure/IsaMakefile	Mon Feb 11 10:56:33 2002 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Mon Feb 11 17:30:58 2002 +0100
     1.3 @@ -40,20 +40,20 @@
     1.4    Isar/rule_cases.ML Isar/session.ML Isar/skip_proof.ML			\
     1.5    Isar/thy_header.ML Isar/toplevel.ML ML-Systems/mlworks.ML		\
     1.6    ML-Systems/polyml-3.x.ML ML-Systems/polyml.ML				\
     1.7 -  ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML Proof/ROOT.ML		\
     1.8 -  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
     1.9 -  Proof/proofchecker.ML Proof/reconstruct.ML ROOT.ML Syntax/ROOT.ML	\
    1.10 -  Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML	\
    1.11 -  Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML		\
    1.12 -  Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML		\
    1.13 -  Thy/ROOT.ML Thy/html.ML Thy/latex.ML Thy/present.ML			\
    1.14 -  Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML Thy/thy_load.ML	\
    1.15 -  Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML	\
    1.16 -  codegen.ML context.ML display.ML drule.ML envir.ML goals.ML		\
    1.17 -  install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML		\
    1.18 -  pattern.ML proof_general.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML		\
    1.19 -  sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML	\
    1.20 -  thm.ML type.ML type_infer.ML unify.ML
    1.21 +  ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-0.93.ML                 \
    1.22 +  ML-Systems/smlnj.ML Proof/ROOT.ML Proof/proof_rewrite_rules.ML        \
    1.23 +  Proof/proof_syntax.ML	Proof/proofchecker.ML Proof/reconstruct.ML      \
    1.24 +  ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML                \
    1.25 +  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML \
    1.26 +  Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML            \
    1.27 +  Syntax/type_ext.ML Thy/ROOT.ML Thy/html.ML Thy/latex.ML               \
    1.28 +  Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML    \
    1.29 +  Thy/thy_load.ML Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML       \
    1.30 +  axclass.ML basis.ML codegen.ML context.ML display.ML drule.ML         \
    1.31 +  envir.ML goals.ML install_pp.ML library.ML logic.ML                   \
    1.32 +  meta_simplifier.ML net.ML pattern.ML proof_general.ML proofterm.ML    \
    1.33 +  pure.ML pure_thy.ML search.ML sign.ML sorts.ML tactic.ML tctical.ML   \
    1.34 +  term.ML theory.ML theory_data.ML thm.ML type.ML type_infer.ML unify.ML
    1.35  	@./mk
    1.36  
    1.37  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/smlnj-compiler.ML	Mon Feb 11 17:30:58 2002 +0100
     2.3 @@ -0,0 +1,15 @@
     2.4 +(*  Title:      Pure/ML-Systems/smlnj.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Markus Wenzel, LMU Muenchen
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8 +
     2.9 +Compatibility tweak for later versions of Standard ML of New Jersey 110.
    2.10 +*)
    2.11 +
    2.12 +structure Compiler =
    2.13 +struct
    2.14 +  structure Control = Control;
    2.15 +  structure PrettyPrint = PrettyPrint;
    2.16 +  structure PPTable = CompilerPPTable;
    2.17 +  structure Interact = Backend.Interact;
    2.18 +end;

     3.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Feb 11 10:56:33 2002 +0100
     3.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Feb 11 17:30:58 2002 +0100
     3.3 @@ -1,10 +1,16 @@
     3.4  (*  Title:      Pure/ML-Systems/smlnj.ML
     3.5      ID:         $Id$
     3.6      Author:     Carsten Clasohm and Markus Wenzel, TU Muenchen
     3.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.8  
     3.9  Compatibility file for Standard ML of New Jersey 110 or later.
    3.10  *)
    3.11  
    3.12 +(case #version_id (Compiler.version) of
    3.13 +  [110, x] => if x >= 35 then use "ML-Systems/smlnj-compiler.ML" else ()
    3.14 +| _ => ());
    3.15 +
    3.16 +
    3.17  (** ML system related **)
    3.18  
    3.19  (* restore old-style character / string functions *)