src/Pure/Concurrent/future.ML
changeset 37216 3165bc303f66
parent 37182 71c8565dae38
child 37698 ad5489a6be48
     1.1 --- a/src/Pure/Concurrent/future.ML	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4    val lock = Mutex.mutex ();
     1.5  in
     1.6  
     1.7 -fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
     1.8 +fun SYNCHRONIZED name = Simple_Thread.synchronized name lock;
     1.9  
    1.10  fun wait cond = (*requires SYNCHRONIZED*)
    1.11    Multithreading.sync_wait NONE NONE cond lock;
    1.12 @@ -238,7 +238,7 @@
    1.13    | SOME work => (execute work; worker_loop name));
    1.14  
    1.15  fun worker_start name = (*requires SYNCHRONIZED*)
    1.16 -  Unsynchronized.change workers (cons (SimpleThread.fork false (fn () => worker_loop name),
    1.17 +  Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
    1.18      Unsynchronized.ref Working));
    1.19  
    1.20  
    1.21 @@ -371,7 +371,7 @@
    1.22  fun scheduler_check () = (*requires SYNCHRONIZED*)
    1.23   (do_shutdown := false;
    1.24    if scheduler_active () then ()
    1.25 -  else scheduler := SOME (SimpleThread.fork false scheduler_loop));
    1.26 +  else scheduler := SOME (Simple_Thread.fork false scheduler_loop));
    1.27  
    1.28  
    1.29