# HG changeset patch # User wenzelm # Date 1313681447 -7200 # Node ID 3ff2fd162aeed58e88f44eae59105add1c6fef5c # Parent f6a11c1da8219a9b8dbd6da5c52c52cc47f15727 updated sequential version (cf. b94951f06e48); diff -r f6a11c1da821 -r 3ff2fd162aee src/Pure/Concurrent/par_list_sequential.ML --- a/src/Pure/Concurrent/par_list_sequential.ML Thu Aug 18 16:07:58 2011 +0200 +++ b/src/Pure/Concurrent/par_list_sequential.ML Thu Aug 18 17:30:47 2011 +0200 @@ -7,6 +7,7 @@ structure Par_List: PAR_LIST = struct +fun managed_results _ f = map (Exn.capture f); fun map_name _ = map; val map = map; val get_some = get_first;