src/Pure/ROOT.ML
changeset 32840 75dff0bd4d5d
parent 32816 5db89f8d44f3
child 33374 8099185908a4
--- a/src/Pure/ROOT.ML	Thu Oct 01 20:47:26 2009 +0200
+++ b/src/Pure/ROOT.ML	Thu Oct 01 22:39:06 2009 +0200
@@ -56,19 +56,25 @@
 (* concurrency within the ML runtime *)
 
 use "Concurrent/simple_thread.ML";
+
 use "Concurrent/synchronized.ML";
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
+
 use "Concurrent/mailbox.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
+
 use "Concurrent/lazy.ML";
 if Multithreading.available then ()
 else use "Concurrent/lazy_sequential.ML";
+
 use "Concurrent/par_list.ML";
 if Multithreading.available then ()
 else use "Concurrent/par_list_sequential.ML";
 
+use "Concurrent/cache.ML";
+
 
 (* fundamental structures *)