author | wenzelm |
Thu, 18 Aug 2011 17:30:47 +0200 | |
changeset 45152 | 3ff2fd162aee |
parent 45151 | f6a11c1da821 |
child 45153 | 3eaad39e520c |
1.1 --- a/src/Pure/Concurrent/par_list_sequential.ML Thu Aug 18 16:07:58 2011 +0200 1.2 +++ b/src/Pure/Concurrent/par_list_sequential.ML Thu Aug 18 17:30:47 2011 +0200 1.3 @@ -7,6 +7,7 @@ 1.4 structure Par_List: PAR_LIST = 1.5 struct 1.6 1.7 +fun managed_results _ f = map (Exn.capture f); 1.8 fun map_name _ = map; 1.9 val map = map; 1.10 val get_some = get_first;