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 =