src/Pure/ROOT.ML
changeset 52798 9d3c9862d1dd
parent 52788 da1fdbfebd39
child 52836 1a03ffc00a4a
     1.1 --- a/src/Pure/ROOT.ML	Tue Jul 30 16:22:07 2013 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Jul 30 18:19:16 2013 +0200
     1.3 @@ -70,8 +70,6 @@
     1.4  
     1.5  (* concurrency within the ML runtime *)
     1.6  
     1.7 -use "Concurrent/event_timer.ML";
     1.8 -
     1.9  if ML_System.is_polyml
    1.10  then use "ML/exn_properties_polyml.ML"
    1.11  else use "ML/exn_properties_dummy.ML";
    1.12 @@ -84,8 +82,6 @@
    1.13  if Multithreading.available then ()
    1.14  else use "Concurrent/single_assignment_sequential.ML";
    1.15  
    1.16 -if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
    1.17 -
    1.18  if Multithreading.available
    1.19  then use "Concurrent/bash.ML"
    1.20  else use "Concurrent/bash_sequential.ML";
    1.21 @@ -93,6 +89,9 @@
    1.22  use "Concurrent/par_exn.ML";
    1.23  use "Concurrent/task_queue.ML";
    1.24  use "Concurrent/future.ML";
    1.25 +use "Concurrent/event_timer.ML";
    1.26 +
    1.27 +if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
    1.28  
    1.29  use "Concurrent/lazy.ML";
    1.30  if Multithreading.available then ()