1.1 --- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 15:37:01 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 15:39:00 2011 +0200
     1.3 @@ -47,19 +47,19 @@
     1.4  
     1.5  (* parallel results *)
     1.6  
     1.7 -fun all_res results = forall (fn Exn.Res _ => true | _ => false) results;
     1.8 -
     1.9  fun release_all results =
    1.10 -  if all_res results then map Exn.release results
    1.11 +  if forall (fn Exn.Res _ => true | _ => false) results
    1.12 +  then map Exn.release results
    1.13    else raise make (map_filter Exn.get_exn results);
    1.14  
    1.15 +fun plain_exn (Exn.Res _) = NONE
    1.16 +  | plain_exn (Exn.Exn (Par_Exn _)) = NONE
    1.17 +  | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
    1.18 +
    1.19  fun release_first results =
    1.20 -  if all_res results then map Exn.release results
    1.21 -  else
    1.22 -    (case get_first
    1.23 -        (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
    1.24 -      NONE => Exn.interrupt ()
    1.25 -    | SOME exn => reraise exn);
    1.26 +  (case get_first plain_exn results of
    1.27 +    NONE => release_all results
    1.28 +  | SOME exn => reraise exn);
    1.29  
    1.30  end;
    1.31