src/Pure/ROOT.ML
changeset 35014 a725ff6ead26
parent 33538 edf497b5b5d2
child 35626 06197484c6ad
--- a/src/Pure/ROOT.ML	Sat Feb 06 20:57:07 2010 +0100
+++ b/src/Pure/ROOT.ML	Sat Feb 06 22:01:48 2010 +0100
@@ -57,6 +57,10 @@
 
 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";