changeset 44269 | 3ff2fd162aee |
parent 41711 | 3422ae5aff3a |
child 59004 | 6573e6d64ec8 |
--- 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;