ML-Systems/smlnj-compiler.ML compatibility tweak;

--- a/src/Pure/IsaMakefile	Mon Feb 11 10:56:33 2002 +0100
+++ b/src/Pure/IsaMakefile	Mon Feb 11 17:30:58 2002 +0100
@@ -40,20 +40,20 @@
   Isar/rule_cases.ML Isar/session.ML Isar/skip_proof.ML			\
   Isar/thy_header.ML Isar/toplevel.ML ML-Systems/mlworks.ML		\
   ML-Systems/polyml-3.x.ML ML-Systems/polyml.ML				\
-  ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML Proof/ROOT.ML		\
-  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
-  Proof/proofchecker.ML Proof/reconstruct.ML ROOT.ML Syntax/ROOT.ML	\
-  Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML	\
-  Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML		\
-  Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML		\
-  Thy/ROOT.ML Thy/html.ML Thy/latex.ML Thy/present.ML			\
-  Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML Thy/thy_load.ML	\
-  Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML	\
-  codegen.ML context.ML display.ML drule.ML envir.ML goals.ML		\
-  install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML		\
-  pattern.ML proof_general.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML		\
-  sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML	\
-  thm.ML type.ML type_infer.ML unify.ML
+  ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-0.93.ML                 \
+  ML-Systems/smlnj.ML Proof/ROOT.ML Proof/proof_rewrite_rules.ML        \
+  Proof/proof_syntax.ML	Proof/proofchecker.ML Proof/reconstruct.ML      \
+  ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML                \
+  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML \
+  Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML            \
+  Syntax/type_ext.ML Thy/ROOT.ML Thy/html.ML Thy/latex.ML               \
+  Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML    \
+  Thy/thy_load.ML Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML       \
+  axclass.ML basis.ML codegen.ML context.ML display.ML drule.ML         \
+  envir.ML goals.ML install_pp.ML library.ML logic.ML                   \
+  meta_simplifier.ML net.ML pattern.ML proof_general.ML proofterm.ML    \
+  pure.ML pure_thy.ML search.ML sign.ML sorts.ML tactic.ML tctical.ML   \
+  term.ML theory.ML theory_data.ML thm.ML type.ML type_infer.ML unify.ML
 	@./mk
 
 

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

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