src/Pure/Concurrent/par_list.ML
changeset 44247 270366301bd7
parent 44113 0baa8bbd355a
child 44265 b94951f06e48
--- a/src/Pure/Concurrent/par_list.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -41,7 +41,7 @@
         handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
     in results end;
 
-fun map_name name f xs = Exn.release_first (managed_results name f xs);
+fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
 fun map f = map_name "Par_List.map" f;
 
 fun get_some f xs =
@@ -55,7 +55,7 @@
   in
     (case get_first found results of
       SOME y => SOME y
-    | NONE => (Exn.release_first results; NONE))
+    | NONE => (Par_Exn.release_first results; NONE))
   end;
 
 fun find_some P = get_some (fn x => if P x then SOME x else NONE);