equal
deleted
inserted
replaced
117 structure Mk_Builtins = Generic_Data |
117 structure Mk_Builtins = Generic_Data |
118 ( |
118 ( |
119 type T = (int * mk_builtins) list |
119 type T = (int * mk_builtins) list |
120 val empty = [] |
120 val empty = [] |
121 val extend = I |
121 val extend = I |
122 fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1 |
122 fun merge data = Ord_List.merge fst_int_ord data |
123 ) |
123 ) |
124 |
124 |
125 fun add_mk_builtins mk = |
125 fun add_mk_builtins mk = |
126 Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) |
126 Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) |
127 |
127 |