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