export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;

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