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