src/HOL/Tools/inductive_package.ML
changeset 6729 b6e167580a32
parent 6723 f342449d73ca
child 6851 526c0b90bcef
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue May 25 20:23:30 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue May 25 20:24:10 1999 +0200
     1.3 @@ -710,10 +710,11 @@
     1.4    #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
     1.5  
     1.6  fun ind_decl coind =
     1.7 -  Scan.repeat1 P.term --
     1.8 -  (P.$$$ "intrs" |-- P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term))) --
     1.9 -  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
    1.10 -  Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) []
    1.11 +  (Scan.repeat1 P.term --| P.marg_comment) --
    1.12 +  (P.$$$ "intrs" |--
    1.13 +    P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment))) --
    1.14 +  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
    1.15 +  Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
    1.16    >> (Toplevel.theory o mk_ind coind);
    1.17  
    1.18  val inductiveP =