1.1 --- a/src/Pure/Concurrent/par_exn.ML	Sat Aug 20 19:21:03 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/par_exn.ML	Sat Aug 20 20:00:55 2011 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
     1.5  
     1.6  fun make exns =
     1.7 -  (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
     1.8 +  (case Ord_List.unions exn_ord (map par_exns exns) of
     1.9      [] => Exn.Interrupt
    1.10    | es => Par_Exn es);
    1.11