src/Pure/ROOT.ML
changeset 38874 4a4d34d2f97b
parent 38634 bff9c05fe229
child 38978 4bf80c23320e
     1.1 --- a/src/Pure/ROOT.ML	Mon Aug 30 14:56:27 2010 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Aug 30 15:09:20 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 +use "ML/ml_compiler.ML";
     1.8  if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
     1.9 -  String.isPrefix "smlnj" ml_system
    1.10 -then use "ML/ml_compiler.ML"
    1.11 +  String.isPrefix "smlnj" ml_system then ()
    1.12  else use "ML/ml_compiler_polyml-5.3.ML";
    1.13  use "ML/ml_context.ML";
    1.14