equal
deleted
inserted
replaced
420 Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) [] |
420 Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) [] |
421 >> (Toplevel.theory o mk_datatype); |
421 >> (Toplevel.theory o mk_datatype); |
422 |
422 |
423 val coind_prefix = if coind then "co" else ""; |
423 val coind_prefix = if coind then "co" else ""; |
424 |
424 |
425 val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype") |
425 val _ = OuterSyntax.command (coind_prefix ^ "datatype") |
426 ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl; |
426 ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl; |
427 |
427 |
428 val _ = OuterSyntax.add_parsers [inductiveP]; |
|
429 |
|
430 end; |
428 end; |
431 |
429 |
432 end; |
430 end; |
433 |
431 |