| changeset 47823 | 94aa7b81bcf6 |
| parent 47780 | 3c73a121a387 |
| child 47836 | 5c6955f487e5 |
| 47822:aae5566d6756 | 47823:94aa7b81bcf6 |
|---|---|
760 local |
760 local |
761 |
761 |
762 val parse_domain_iso : |
762 val parse_domain_iso : |
763 (string list * binding * mixfix * string * (binding * binding) option) |
763 (string list * binding * mixfix * string * (binding * binding) option) |
764 parser = |
764 parser = |
765 (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) -- |
765 (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- |
766 Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))) |
766 Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))) |
767 >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)) |
767 >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)) |
768 |
768 |
769 val parse_domain_isos = Parse.and_list1 parse_domain_iso |
769 val parse_domain_isos = Parse.and_list1 parse_domain_iso |
770 |
770 |
771 in |
771 in |