--- a/src/Pure/Concurrent/schedule.ML Tue Sep 16 15:37:32 2008 +0200
+++ b/src/Pure/Concurrent/schedule.ML Tue Sep 16 15:37:33 2008 +0200
@@ -53,12 +53,8 @@
(*pool of running threads*)
val status = ref ([]: exn list);
val running = ref ([]: Thread.thread list);
- fun start f =
- (inc active;
- change running (cons (Thread.fork (f, Multithreading.no_interrupts))));
- fun stop () =
- (dec active;
- change running (filter (fn t => not (Thread.equal (t, Thread.self ())))));
+ fun start f = (inc active; change running (cons (SimpleThread.fork false f)));
+ fun stop () = (dec active; change running (remove Thread.equal (Thread.self ())));
(*worker thread*)
fun worker () =