src/Pure/ML-Systems/smlnj.ML
changeset 12874 368966ceafe5
parent 12581 dceea9dbdedd
child 12990 c11adf2b1c1e
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Feb 11 10:56:33 2002 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Feb 11 17:30:58 2002 +0100
     1.3 @@ -1,10 +1,16 @@
     1.4  (*  Title:      Pure/ML-Systems/smlnj.ML
     1.5      ID:         $Id$
     1.6      Author:     Carsten Clasohm and Markus Wenzel, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8  
     1.9  Compatibility file for Standard ML of New Jersey 110 or later.
    1.10  *)
    1.11  
    1.12 +(case #version_id (Compiler.version) of
    1.13 +  [110, x] => if x >= 35 then use "ML-Systems/smlnj-compiler.ML" else ()
    1.14 +| _ => ());
    1.15 +
    1.16 +
    1.17  (** ML system related **)
    1.18  
    1.19  (* restore old-style character / string functions *)