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