# 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;