src/Pure/ROOT.ML
changeset 44247 270366301bd7
parent 44185 05641edb5d30
child 44549 5e5e6ad3922c
     1.1 --- a/src/Pure/ROOT.ML	Wed Aug 17 20:08:36 2011 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Aug 17 22:14:22 2011 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4  then use "Concurrent/bash.ML"
     1.5  else use "Concurrent/bash_sequential.ML";
     1.6  
     1.7 -use "Concurrent/mailbox.ML";
     1.8 +use "Concurrent/par_exn.ML";
     1.9  use "Concurrent/task_queue.ML";
    1.10  use "Concurrent/future.ML";
    1.11  
    1.12 @@ -89,6 +89,7 @@
    1.13  if Multithreading.available then ()
    1.14  else use "Concurrent/par_list_sequential.ML";
    1.15  
    1.16 +use "Concurrent/mailbox.ML";
    1.17  use "Concurrent/cache.ML";
    1.18  
    1.19