--- 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);