Ord_List.merge convenience;

--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Sat Jan 08 17:14:48 2011 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Sat Jan 08 17:30:05 2011 +0100
@@ -278,7 +278,7 @@
   type T = (serial * (term -> bool)) Ord_List.T
   val empty = []
   val extend = I
-  fun merge (fs1, fs2) = fold (Ord_List.insert serial_ord) fs2 fs1
+  fun merge data = Ord_List.merge serial_ord data
 )
 
 fun add_assertion_filter f =

--- a/src/HOL/Tools/SMT/smt_builtin.ML	Sat Jan 08 17:14:48 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Sat Jan 08 17:30:05 2011 +0100
@@ -70,7 +70,7 @@
     (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
 
 fun merge_ttab ttabp =
-  SMT_Utils.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp
+  SMT_Utils.dict_merge (Ord_List.merge typ_ord) ttabp
 
 fun lookup_ttab ctxt ttab T =
   let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)

--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sat Jan 08 17:14:48 2011 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Sat Jan 08 17:30:05 2011 +0100
@@ -81,7 +81,7 @@
   type T = (int * (term list -> string option)) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
+  fun merge data = Ord_List.merge fst_int_ord data
 )
 
 fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)

--- a/src/HOL/Tools/SMT/z3_interface.ML	Sat Jan 08 17:14:48 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Sat Jan 08 17:30:05 2011 +0100
@@ -119,7 +119,7 @@
   type T = (int * mk_builtins) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
+  fun merge data = Ord_List.merge fst_int_ord data
 )
 
 fun add_mk_builtins mk =

--- a/src/Pure/General/ord_list.ML	Sat Jan 08 17:14:48 2011 +0100
+++ b/src/Pure/General/ord_list.ML	Sat Jan 08 17:30:05 2011 +0100
@@ -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 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
 end;
@@ -85,6 +86,8 @@
           | GREATER => y :: unio lst1 ys);
   in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
 
+fun merge ord (list1, list2) = union ord list2 list1;
+
 (*intersection: filter second list for elements present in first list*)
 fun inter ord list1 list2 =
   let