| changeset 18970 | d055a29ddd23 |
| parent 18921 | f47c46d7d654 |
| child 19029 | 8635700e2c9c |
| 18969:49aa2c8791ba | 18970:d055a29ddd23 |
|---|---|
51 |
51 |
52 (* keys *) |
52 (* keys *) |
53 |
53 |
54 type key = Key.key; |
54 type key = Key.key; |
55 |
55 |
56 val eq_key = equal EQUAL o Key.ord; |
56 val eq_key = is_equal o Key.ord; |
57 |
57 |
58 val member_key = member eq_key; |
58 val member_key = member eq_key; |
59 val remove_key = remove eq_key; |
59 val remove_key = remove eq_key; |
60 |
60 |
61 |
61 |