equal
deleted
inserted
replaced
786 |
786 |
787 (* outer syntax *) |
787 (* outer syntax *) |
788 |
788 |
789 val spec_cmd = |
789 val spec_cmd = |
790 Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix -- |
790 Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix -- |
791 (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix)) |
791 (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix)) |
792 >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons)); |
792 >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons)); |
793 |
793 |
794 val _ = |
794 val _ = |
795 Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl |
795 Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl |
796 (Parse.and_list1 spec_cmd |
796 (Parse.and_list1 spec_cmd |