src/Pure/ROOT.ML
changeset 41718 05514b09bb4b
parent 41710 11ae688e4e30
child 42012 2c3fe3cbebae
--- a/src/Pure/ROOT.ML	Tue Feb 08 17:27:18 2011 +0100
+++ b/src/Pure/ROOT.ML	Tue Feb 08 17:36:21 2011 +0100
@@ -72,9 +72,8 @@
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
 
-use "Concurrent/time_limit.ML";
-if Multithreading.available then ()
-else use "Concurrent/time_limit_dummy.ML";
+if String.isPrefix "smlnj" ml_system then ()
+else use "Concurrent/time_limit.ML";
 
 if Multithreading.available
 then use "Concurrent/bash.ML"
@@ -193,8 +192,7 @@
 use "ML/ml_env.ML";
 use "Isar/runtime.ML";
 use "ML/ml_compiler.ML";
-if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
-  String.isPrefix "smlnj" ml_system then ()
+if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then ()
 else use "ML/ml_compiler_polyml-5.3.ML";
 use "ML/ml_context.ML";