equal
deleted
inserted
replaced
61 type keys = unit Table.table; |
61 type keys = unit Table.table; |
62 |
62 |
63 val empty_keys = Table.empty: keys; |
63 val empty_keys = Table.empty: keys; |
64 |
64 |
65 infix mem_keys; |
65 infix mem_keys; |
66 fun x mem_keys tab = is_some (Table.lookup (tab: keys, x)); |
66 fun x mem_keys tab = Table.defined (tab: keys) x; |
67 |
67 |
68 infix ins_keys; |
68 infix ins_keys; |
69 fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys); |
69 fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys); |
70 |
70 |
71 |
71 |