1.1 --- a/src/Pure/ROOT.ML	Tue Feb 08 17:27:18 2011 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Tue Feb 08 17:36:21 2011 +0100
     1.3 @@ -72,9 +72,8 @@
     1.4  if Multithreading.available then ()
     1.5  else use "Concurrent/synchronized_sequential.ML";
     1.6  
     1.7 -use "Concurrent/time_limit.ML";
     1.8 -if Multithreading.available then ()
     1.9 -else use "Concurrent/time_limit_dummy.ML";
    1.10 +if String.isPrefix "smlnj" ml_system then ()
    1.11 +else use "Concurrent/time_limit.ML";
    1.12  
    1.13  if Multithreading.available
    1.14  then use "Concurrent/bash.ML"
    1.15 @@ -193,8 +192,7 @@
    1.16  use "ML/ml_env.ML";
    1.17  use "Isar/runtime.ML";
    1.18  use "ML/ml_compiler.ML";
    1.19 -if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
    1.20 -  String.isPrefix "smlnj" ml_system then ()
    1.21 +if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then ()
    1.22  else use "ML/ml_compiler_polyml-5.3.ML";
    1.23  use "ML/ml_context.ML";
    1.24