1.1 --- a/src/Pure/ROOT.ML	Wed Jul 06 20:14:13 2011 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Jul 06 20:46:06 2011 +0200
     1.3 @@ -20,6 +20,13 @@
     1.4  use "General/print_mode.ML";
     1.5  use "General/alist.ML";
     1.6  use "General/table.ML";
     1.7 +
     1.8 +use "Concurrent/simple_thread.ML";
     1.9 +
    1.10 +use "Concurrent/synchronized.ML";
    1.11 +if Multithreading.available then ()
    1.12 +else use "Concurrent/synchronized_sequential.ML";
    1.13 +
    1.14  use "General/output.ML";
    1.15  use "General/timing.ML";
    1.16  use "General/properties.ML";
    1.17 @@ -63,16 +70,10 @@
    1.18  
    1.19  (* concurrency within the ML runtime *)
    1.20  
    1.21 -use "Concurrent/simple_thread.ML";
    1.22 -
    1.23  use "Concurrent/single_assignment.ML";
    1.24  if Multithreading.available then ()
    1.25  else use "Concurrent/single_assignment_sequential.ML";
    1.26  
    1.27 -use "Concurrent/synchronized.ML";
    1.28 -if Multithreading.available then ()
    1.29 -else use "Concurrent/synchronized_sequential.ML";
    1.30 -
    1.31  if String.isPrefix "smlnj" ml_system then ()
    1.32  else use "Concurrent/time_limit.ML";
    1.33