src/Pure/ROOT.ML
changeset 43684 85388f5570c4
parent 43593 11140987d415
child 43712 3c2c912af2ef
--- a/src/Pure/ROOT.ML	Wed Jul 06 20:14:13 2011 +0200
+++ b/src/Pure/ROOT.ML	Wed Jul 06 20:46:06 2011 +0200
@@ -20,6 +20,13 @@
 use "General/print_mode.ML";
 use "General/alist.ML";
 use "General/table.ML";
+
+use "Concurrent/simple_thread.ML";
+
+use "Concurrent/synchronized.ML";
+if Multithreading.available then ()
+else use "Concurrent/synchronized_sequential.ML";
+
 use "General/output.ML";
 use "General/timing.ML";
 use "General/properties.ML";
@@ -63,16 +70,10 @@
 
 (* concurrency within the ML runtime *)
 
-use "Concurrent/simple_thread.ML";
-
 use "Concurrent/single_assignment.ML";
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";
 
-use "Concurrent/synchronized.ML";
-if Multithreading.available then ()
-else use "Concurrent/synchronized_sequential.ML";
-
 if String.isPrefix "smlnj" ml_system then ()
 else use "Concurrent/time_limit.ML";