diff -r 296b478df14e -r e6e5750f1311 src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Mon Apr 09 15:10:52 2012 +0200 +++ b/src/Pure/Concurrent/par_list.ML Mon Apr 09 17:22:23 2012 +0200 @@ -39,8 +39,7 @@ 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 ignore (Future.cancel_group group) else (); reraise exn); + handle exn => (if Exn.is_interrupt exn then 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);