src/Pure/Concurrent/par_list.ML

--- a/src/Pure/Concurrent/par_list.ML	Fri Aug 19 14:01:20 2011 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Fri Aug 19 15:56:26 2011 +0200
@@ -39,7 +39,8 @@
         Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
           (map (fn x => fn () => f x) xs);
       val results = Future.join_results futures
-        handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+        handle exn =>
+          (if Exn.is_interrupt exn then ignore (Future.cancel_group group) else (); reraise exn);
     in results end;
 
 fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);