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