# HG changeset patch
# User wenzelm
# Date 1313863255 -7200
# Node ID 605381e7c7c5e7afba651c5e3ea68c4830f4b2c9
# Parent  cc53ce50f738f59865cdf49769140b8fa05322a3
more direct balanced version Ord_List.unions;

diff -r cc53ce50f738 -r 605381e7c7c5 Admin/polyml/future/ROOT.ML
--- a/Admin/polyml/future/ROOT.ML	Sat Aug 20 19:21:03 2011 +0200
+++ b/Admin/polyml/future/ROOT.ML	Sat Aug 20 20:00:55 2011 +0200
@@ -78,7 +78,6 @@
 use "General/table.ML";
 use "General/graph.ML";
 use "General/ord_list.ML";
-use "General/balanced_tree.ML";
 
 structure Position =
 struct
diff -r cc53ce50f738 -r 605381e7c7c5 src/Pure/Concurrent/par_exn.ML
--- 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);
 
diff -r cc53ce50f738 -r 605381e7c7c5 src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Sat Aug 20 19:21:03 2011 +0200
+++ b/src/Pure/General/ord_list.ML	Sat Aug 20 20:00:55 2011 +0200
@@ -14,6 +14,7 @@
   val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
   val subset: ('b * 'a -> order) -> 'b T * 'a T -> bool
   val union: ('a * 'a -> order) -> 'a T -> 'a T -> 'a T
+  val unions: ('a * 'a -> order) -> 'a T list -> 'a T
   val merge: ('a * 'a -> order) -> 'a T * 'a T -> 'a T
   val inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
   val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
@@ -86,6 +87,15 @@
           | GREATER => y :: unio lst1 ys);
   in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
 
+fun unions ord lists =
+  let
+    fun unios (xs :: ys :: rest) acc = unios rest (union ord xs ys :: acc)
+      | unios [xs] (ys :: acc) = unios (union ord xs ys :: acc) []
+      | unios [xs] [] = xs
+      | unios [] [] = []
+      | unios [] acc = unios acc [];
+  in unios lists [] end;
+
 fun merge ord (list1, list2) = union ord list2 list1;
 
 (*intersection: filter second list for elements present in first list*)
diff -r cc53ce50f738 -r 605381e7c7c5 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Aug 20 19:21:03 2011 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 20 20:00:55 2011 +0200
@@ -46,8 +46,8 @@
 
   val oracle_ord: oracle * oracle -> order
   val thm_ord: pthm * pthm -> order
-  val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
-  val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
+  val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
+  val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
   val all_oracles_of: proof_body -> oracle Ord_List.T
   val approximate_proof_body: proof -> proof_body
 
@@ -237,8 +237,8 @@
 val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
 fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
 
-val merge_oracles = Ord_List.union oracle_ord;
-val merge_thms = Ord_List.union thm_ord;
+val unions_oracles = Ord_List.unions oracle_ord;
+val unions_thms = Ord_List.unions thm_ord;
 
 val all_oracles_of =
   let
@@ -249,8 +249,8 @@
           let
             val body' = Future.join body;
             val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
-          in (merge_oracles oracles x', seen') end);
-  in fn body => #1 (collect body ([], Inttab.empty)) end;
+          in (if null oracles then x' else oracles :: x', seen') end);
+  in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
 
 fun approximate_proof_body prf =
   let
@@ -1385,8 +1385,11 @@
 fun fulfill_norm_proof thy ps body0 =
   let
     val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
-    val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
-    val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+    val oracles =
+      unions_oracles
+        (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
+    val thms =
+      unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
     val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
 
     fun fill (Promise (i, prop, Ts)) =
diff -r cc53ce50f738 -r 605381e7c7c5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 20 19:21:03 2011 +0200
+++ b/src/Pure/thm.ML	Sat Aug 20 20:00:55 2011 +0200
@@ -492,8 +492,8 @@
     (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   let
     val ps = Ord_List.union promise_ord ps1 ps2;
-    val oras = Proofterm.merge_oracles oras1 oras2;
-    val thms = Proofterm.merge_thms thms1 thms2;
+    val oras = Proofterm.unions_oracles [oras1, oras2];
+    val thms = Proofterm.unions_thms [thms1, thms2];
     val prf =
       (case ! Proofterm.proofs of
         2 => f prf1 prf2