equal
deleted
inserted
replaced
630 val add_abbrevs = fold o add_abbrev; |
630 val add_abbrevs = fold o add_abbrev; |
631 |
631 |
632 fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal); |
632 fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal); |
633 |
633 |
634 fun merge_types (types1, types2) = |
634 fun merge_types (types1, types2) = |
635 NameSpace.merge_tables Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) => |
635 NameSpace.merge_tables (Library.eq_snd (op =)) (types1, types2) handle Symtab.DUPS (d :: _) => |
636 err_in_decls d (the_decl types1 d) (the_decl types2 d); |
636 err_in_decls d (the_decl types1 d) (the_decl types2 d); |
637 |
637 |
638 end; |
638 end; |
639 |
639 |
640 fun hide_types fully cs = map_tsig (fn (classes, default, (space, types), arities) => |
640 fun hide_types fully cs = map_tsig (fn (classes, default, (space, types), arities) => |