diff -r 0506197d285f -r 3def1a1fea4e src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 11 19:35:05 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 11 20:30:46 2008 +0100
@@ -312,7 +312,9 @@
      (fork (Int.max (n, 1));
       while not (List.null (! running)) do
       (trace_active ();
-       if not (List.null (! status)) then (List.app Thread.interrupt (! running)) else ();
+       if not (List.null (! status))
+       then (List.app (fn t => Thread.interrupt t handle Thread _ => ()) (! running))
+       else ();
        wait_timeout ())));
 
   in ! status end);