src/Pure/Concurrent/par_list.ML
changeset 78705 fde0b195cb7d
parent 73686 b9aae426e51d
--- a/src/Pure/Concurrent/par_list.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -37,7 +37,7 @@
 
 fun map' params f xs = Par_Exn.release_first (managed_results params f xs);
 fun map f = map' {name = "", sequential = false} f;
-fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all;
+fun map_independent f = map (Exn.result f) #> Par_Exn.release_all;
 
 fun get_some f xs =
   let