1.1 --- a/Admin/polyml/future/ROOT.ML	Thu Aug 18 16:52:19 2011 +0900
     1.2 +++ b/Admin/polyml/future/ROOT.ML	Thu Aug 18 15:15:43 2011 +0200
     1.3 @@ -78,6 +78,7 @@
     1.4  use "General/table.ML";
     1.5  use "General/graph.ML";
     1.6  use "General/ord_list.ML";
     1.7 +use "General/balanced_tree.ML";
     1.8  
     1.9  structure Position =
    1.10  struct

     2.1 --- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 16:52:19 2011 +0900
     2.2 +++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 15:15:43 2011 +0200
     2.3 @@ -29,17 +29,19 @@
     2.4  
     2.5  (* parallel exceptions *)
     2.6  
     2.7 -exception Par_Exn of exn Ord_List.T;
     2.8 +exception Par_Exn of exn list;
     2.9 +  (*non-empty list with unique identified elements sorted by exn_ord;
    2.10 +    no occurrences of Par_Exn or Exn.Interrupt*)
    2.11  
    2.12 -fun par_exns (Par_Exn exns) = SOME exns
    2.13 -  | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)];
    2.14 +fun par_exns (Par_Exn exns) = exns
    2.15 +  | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
    2.16  
    2.17  fun make exns =
    2.18 -  (case map_filter par_exns exns of
    2.19 +  (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
    2.20      [] => Exn.Interrupt
    2.21 -  | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es)));
    2.22 +  | es => Par_Exn es);
    2.23  
    2.24 -fun dest (Par_Exn exns) = SOME (rev exns)
    2.25 +fun dest (Par_Exn exns) = SOME exns
    2.26    | dest _ = NONE;
    2.27  
    2.28  

     3.1 --- a/src/Pure/Isar/runtime.ML	Thu Aug 18 16:52:19 2011 +0900
     3.2 +++ b/src/Pure/Isar/runtime.ML	Thu Aug 18 15:15:43 2011 +0200
     3.3 @@ -61,7 +61,7 @@
     3.4        if Exn.is_interrupt exn then []
     3.5        else
     3.6          (case Par_Exn.dest exn of
     3.7 -          SOME exns => maps (exn_msgs context) exns
     3.8 +          SOME exns => maps (exn_msgs context) (rev exns)
     3.9          | NONE =>
    3.10              (case exn of
    3.11                Exn.EXCEPTIONS exns => maps (exn_msgs context) exns