1.1 --- a/src/Pure/Concurrent/simple_thread.ML Tue Oct 27 10:54:25 2009 +0100
1.2 +++ b/src/Pure/Concurrent/simple_thread.ML Tue Oct 27 11:25:56 2009 +0100
1.3 @@ -15,7 +15,7 @@
1.4 struct
1.5
1.6 fun fork interrupts body =
1.7 - Thread.fork (fn () => exception_trace (fn () => body ()),
1.8 + Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
1.9 if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
1.10
1.11 fun interrupt thread = Thread.interrupt thread handle Thread _ => ();