equal
deleted
inserted
replaced
251 fun extend_prtabs m = change_prtabs Symtab.update_list m; |
251 fun extend_prtabs m = change_prtabs Symtab.update_list m; |
252 fun remove_prtabs m = change_prtabs (Symtab.remove_list (op =)) m; |
252 fun remove_prtabs m = change_prtabs (Symtab.remove_list (op =)) m; |
253 |
253 |
254 fun merge_prtabs prtabs1 prtabs2 = |
254 fun merge_prtabs prtabs1 prtabs2 = |
255 let |
255 let |
256 val modes = gen_distinct (op =) (map fst (prtabs1 @ prtabs2)); |
256 val modes = distinct (op =) (map fst (prtabs1 @ prtabs2)); |
257 fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m)); |
257 fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m)); |
258 in map merge modes end; |
258 in map merge modes end; |
259 |
259 |
260 |
260 |
261 |
261 |