src/HOL/Tools/SMT/z3_interface.ML
changeset 41473 3717fc42ebe9
parent 41302 0485186839a7
child 41691 8f0531cf34f8
--- 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 =