src/Pure/Concurrent/par_exn.ML
changeset 44334 605381e7c7c5
parent 44296 0c4411e2fc90
child 47338 e331c6256a41
--- a/src/Pure/Concurrent/par_exn.ML	Sat Aug 20 19:21:03 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Sat Aug 20 20:00:55 2011 +0200
@@ -43,7 +43,7 @@
   | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
 
 fun make exns =
-  (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
+  (case Ord_List.unions exn_ord (map par_exns exns) of
     [] => Exn.Interrupt
   | es => Par_Exn es);