| changeset 19046 | bc5c6c9b114e |
| parent 18977 | f24c416a4814 |
| child 19374 | ae4a225e0c1f |
--- a/src/Pure/Syntax/printer.ML Wed Feb 15 19:11:10 2006 +0100 +++ b/src/Pure/Syntax/printer.ML Wed Feb 15 21:34:55 2006 +0100 @@ -253,7 +253,7 @@ fun merge_prtabs prtabs1 prtabs2 = let - val modes = gen_distinct (op =) (map fst (prtabs1 @ prtabs2)); + val modes = distinct (op =) (map fst (prtabs1 @ prtabs2)); fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m)); in map merge modes end;