diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/Concurrent/simple_thread.ML
--- 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 _ => ();