src/Pure/Concurrent/par_list_sequential.ML
changeset 44269 3ff2fd162aee
parent 41711 3422ae5aff3a
child 59004 6573e6d64ec8
     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;