equal
deleted
inserted
replaced
744 fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps; |
744 fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps; |
745 |
745 |
746 |
746 |
747 fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss |
747 fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss |
748 handle Symtab.DUPS xs => err_in_locale ctxt |
748 handle Symtab.DUPS xs => err_in_locale ctxt |
749 ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map #1 ids); |
749 ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids); |
750 |
750 |
751 |
751 |
752 (* flatten expressions *) |
752 (* flatten expressions *) |
753 |
753 |
754 local |
754 local |