author | wenzelm |
Thu, 18 Aug 2011 17:30:47 +0200 | |
changeset 44269 | 3ff2fd162aee |
parent 44268 | f6a11c1da821 |
child 44270 | 3eaad39e520c |
--- 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;