| changeset 18977 | f24c416a4814 |
| parent 18957 | 8c3abd63bce3 |
| child 19046 | bc5c6c9b114e |
--- a/src/Pure/Syntax/printer.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/Syntax/printer.ML Wed Feb 08 14:39:00 2006 +0100 @@ -253,7 +253,7 @@ fun merge_prtabs prtabs1 prtabs2 = let - val modes = distinct (map fst (prtabs1 @ prtabs2)); + val modes = gen_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;