--- a/src/Pure/Concurrent/simple_thread.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Thu Sep 09 17:20:27 2010 +0200
@@ -19,7 +19,9 @@
if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
fun fork interrupts body =
- Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
+ Thread.fork (fn () =>
+ exception_trace (fn () =>
+ body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
attributes interrupts);
fun interrupt thread = Thread.interrupt thread handle Thread _ => ();