src/Pure/ROOT.ML
changeset 32815 1a5e364584ae
parent 32738 15bb09ca0378
child 32816 5db89f8d44f3
--- a/src/Pure/ROOT.ML	Thu Oct 01 16:27:13 2009 +0200
+++ b/src/Pure/ROOT.ML	Thu Oct 01 18:10:41 2009 +0200
@@ -45,7 +45,6 @@
 use "General/long_name.ML";
 use "General/binding.ML";
 use "General/name_space.ML";
-use "General/lazy.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/buffer.ML";
@@ -58,12 +57,17 @@
 
 use "Concurrent/simple_thread.ML";
 use "Concurrent/synchronized.ML";
-if Multithreading.available then () else use "Concurrent/synchronized_dummy.ML";
+if Multithreading.available then () else
+use "Concurrent/synchronized_dummy.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_dummy.ML";
+if Multithreading.available then ()
+else use "Concurrent/par_list_dummy.ML";
 
 
 (* fundamental structures *)