src/Pure/ROOT.ML
changeset 38470 484e483eb606
parent 38448 62d16c415019
child 38483 3d16bebee1d3
     1.1 --- a/src/Pure/ROOT.ML	Tue Aug 17 18:04:08 2010 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Aug 17 18:41:55 2010 +0200
     1.3 @@ -179,9 +179,9 @@
     1.4  use "ML/ml_syntax.ML";
     1.5  use "ML/ml_env.ML";
     1.6  use "Isar/runtime.ML";
     1.7 -if ml_system = "polyml-5.3.0"
     1.8 -then use "ML/ml_compiler_polyml-5.3.ML"
     1.9 -else use "ML/ml_compiler.ML";
    1.10 +if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system
    1.11 +then use "ML/ml_compiler.ML"
    1.12 +else use "ML/ml_compiler_polyml-5.3.ML";
    1.13  use "ML/ml_context.ML";
    1.14  
    1.15  (*theory sources*)