1.1 --- a/src/Pure/Concurrent/simple_thread.ML	Thu Oct 09 20:53:16 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Thu Oct 09 20:53:17 2008 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  signature SIMPLE_THREAD =
     1.5  sig
     1.6    val fork: bool -> (unit -> unit) -> Thread.thread
     1.7 +  val interrupt: Thread.thread -> unit
     1.8  end;
     1.9  
    1.10  structure SimpleThread: SIMPLE_THREAD =
    1.11 @@ -17,4 +18,6 @@
    1.12    Thread.fork (fn () => exception_trace (fn () => body ()),
    1.13      if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
    1.14  
    1.15 +fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
    1.16 +
    1.17  end;