| changeset 44265 | b94951f06e48 |
| parent 44247 | 270366301bd7 |
| child 44299 | 061599cb6eb0 |
--- a/src/Pure/Concurrent/par_list.ML Thu Aug 18 15:15:43 2011 +0200 +++ b/src/Pure/Concurrent/par_list.ML Thu Aug 18 15:37:01 2011 +0200 @@ -16,6 +16,7 @@ signature PAR_LIST = sig + val managed_results: string -> ('a -> 'b) -> 'a list -> 'b Exn.result list val map_name: string -> ('a -> 'b) -> 'a list -> 'b list val map: ('a -> 'b) -> 'a list -> 'b list val get_some: ('a -> 'b option) -> 'a list -> 'b option