src/Pure/ROOT.ML
changeset 35014 a725ff6ead26
parent 33538 edf497b5b5d2
child 35626 06197484c6ad
     1.1 --- a/src/Pure/ROOT.ML	Sat Feb 06 20:57:07 2010 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Sat Feb 06 22:01:48 2010 +0100
     1.3 @@ -57,6 +57,10 @@
     1.4  
     1.5  use "Concurrent/simple_thread.ML";
     1.6  
     1.7 +use "Concurrent/single_assignment.ML";
     1.8 +if Multithreading.available then ()
     1.9 +else use "Concurrent/single_assignment_sequential.ML";
    1.10 +
    1.11  use "Concurrent/synchronized.ML";
    1.12  if Multithreading.available then ()
    1.13  else use "Concurrent/synchronized_sequential.ML";