equal
deleted
inserted
replaced
91 fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c)); |
91 fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c)); |
92 |
92 |
93 fun extend_tr'tab tab trfuns = |
93 fun extend_tr'tab tab trfuns = |
94 generic_extend eq_trfuns Symtab.dest_multi Symtab.make_multi tab (map mk_trfun trfuns); |
94 generic_extend eq_trfuns Symtab.dest_multi Symtab.make_multi tab (map mk_trfun trfuns); |
95 |
95 |
96 val merge_tr'tabs = generic_merge eq_trfuns Symtab.dest_multi Symtab.make_multi; |
96 fun merge_tr'tabs tabs = generic_merge eq_trfuns Symtab.dest_multi Symtab.make_multi tabs; |
97 |
97 |
98 |
98 |
99 |
99 |
100 (** tables of token translation functions **) |
100 (** tables of token translation functions **) |
101 |
101 |