Simplified thread fork interface.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/simple_thread.ML	Tue Sep 16 15:37:32 2008 +0200
@@ -0,0 +1,20 @@
+(*  Title:      Pure/Concurrent/simple_thread.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Simplified thread fork interface.
+*)
+
+signature SIMPLE_THREAD =
+sig
+  val fork: bool -> (unit -> unit) -> Thread.thread
+end;
+
+structure SimpleThread: SIMPLE_THREAD =
+struct
+
+fun fork interrupts body =
+  Thread.fork (fn () => exception_trace (fn () => body ()),
+    if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
+
+end;