SimpleThread.fork;

--- a/src/Pure/Concurrent/future.ML	Tue Sep 16 15:37:32 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Sep 16 15:37:33 2008 +0200
@@ -160,8 +160,7 @@
   | SOME work => (execute name work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
-  change workers
-    (cons (Thread.fork (fn () => worker_loop name, Multithreading.no_interrupts), true));
+  change workers (cons (SimpleThread.fork false (fn () => worker_loop name), true));
 
 
 (* scheduler *)
@@ -203,8 +202,7 @@
 
 fun scheduler_check () = SYNCHRONIZED "scheduler_check" (fn () =>
   if not (scheduler_active ()) then
-   (do_shutdown := false;
-    scheduler := SOME (Thread.fork (scheduler_loop, Multithreading.no_interrupts)))
+    (do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop))
   else if ! do_shutdown then error "Scheduler shutdown in progress"
   else ());
 

--- 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 () =

--- a/src/Pure/Tools/isabelle_process.ML	Tue Sep 16 15:37:32 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Tue Sep 16 15:37:33 2008 +0200
@@ -118,10 +118,10 @@
           val path = File.platform_path (Path.explode out);
           val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
           val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
-          val _ = Thread.fork (auto_flush TextIO.stdOut, Multithreading.no_interrupts);
+          val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
         in out_stream end;
-    val _ = Thread.fork (auto_flush out_stream, Multithreading.no_interrupts);
-    val _ = Thread.fork (auto_flush TextIO.stdErr, Multithreading.no_interrupts);
+    val _ = SimpleThread.fork false (auto_flush out_stream);
+    val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   in
     Output.writeln_fn  := message out_stream "A" Markup.writelnN;
     Output.priority_fn := message out_stream "B" Markup.priorityN;