equal
deleted
inserted
replaced
106 >> (fn ("wits", Ts) => Ts |
106 >> (fn ("wits", Ts) => Ts |
107 | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| |
107 | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| |
108 @{keyword "]"} || Scan.succeed []; |
108 @{keyword "]"} || Scan.succeed []; |
109 |
109 |
110 val parse_bnf_axiomatization = |
110 val parse_bnf_axiomatization = |
111 parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- |
111 parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings -- |
112 parse_witTs -- Parse.opt_mixfix; |
112 parse_witTs -- Parse.opt_mixfix; |
113 |
113 |
114 val _ = |
114 val _ = |
115 Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration" |
115 Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration" |
116 (parse_bnf_axiomatization >> |
116 (parse_bnf_axiomatization >> |