src/Pure/Concurrent/par_list.ML
changeset 62505 9e2a65912111
parent 59180 c0fa3b3bdabd
child 62891 7a11ea5c9626
--- a/src/Pure/Concurrent/par_list.ML	Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Thu Mar 03 15:23:02 2016 +0100
@@ -46,7 +46,7 @@
         val results =
           restore_attributes Future.join_results futures
             handle exn =>
-              (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+              (if Exn.is_interrupt exn then Future.cancel_group group else (); Exn.reraise exn);
       in results end) ();
 
 fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);