equal
deleted
inserted
replaced
629 |
629 |
630 (** a datatype antiquotation **) |
630 (** a datatype antiquotation **) |
631 |
631 |
632 local |
632 local |
633 |
633 |
634 val sym_datatype = Pretty.str "\\isacommand{datatype}"; |
634 val sym_datatype = Pretty.command "datatype"; |
635 val sym_binder = Pretty.str "\\ {\\isacharequal}"; |
635 val sym_binder = Pretty.str "\\ {\\isacharequal}"; (*FIXME use proper symbol*) |
636 val sym_sep = Pretty.str "{\\isacharbar}\\ "; |
636 val sym_sep = Pretty.str "{\\isacharbar}\\ "; |
637 |
637 |
638 in |
638 in |
639 |
639 |
640 fun args_datatype (ctxt, args) = |
640 fun args_datatype (ctxt, args) = |