src/Pure/ROOT.ML
changeset 44247 270366301bd7
parent 44185 05641edb5d30
child 44549 5e5e6ad3922c
--- a/src/Pure/ROOT.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -77,7 +77,7 @@
 then use "Concurrent/bash.ML"
 else use "Concurrent/bash_sequential.ML";
 
-use "Concurrent/mailbox.ML";
+use "Concurrent/par_exn.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
 
@@ -89,6 +89,7 @@
 if Multithreading.available then ()
 else use "Concurrent/par_list_sequential.ML";
 
+use "Concurrent/mailbox.ML";
 use "Concurrent/cache.ML";