# HG changeset patch
# User wenzelm
# Date 1282558007 -7200
# Node ID bff9c05fe229af9bd10a8b7f40ae41401ea1366e
# Parent  39412530436f0b6a3e07b310aff6d38e3fa01dff
recognize more "smlnj" variants;

diff -r 39412530436f -r bff9c05fe229 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Aug 23 11:18:38 2010 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 23 12:06:47 2010 +0200
@@ -179,7 +179,8 @@
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
 use "Isar/runtime.ML";
-if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system
+if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
+  String.isPrefix "smlnj" ml_system
 then use "ML/ml_compiler.ML"
 else use "ML/ml_compiler_polyml-5.3.ML";
 use "ML/ml_context.ML";