src/HOL/thy_syntax.ML
changeset 11628 e57a6e51715e
parent 9857 2f994c499bef
child 11804 d69e7acd9380
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Sep 28 19:18:46 2001 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Sep 28 19:19:26 2001 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4          \local\n\
     1.5          \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
     1.6          \  InductivePackage.add_inductive true " ^
     1.7 -        (if coind then "true " else "false ") ^ srec_tms ^ " [] " ^
     1.8 +        (if coind then "true " else "false ") ^ srec_tms ^
     1.9           sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
    1.10          \in\n\
    1.11          \structure " ^ big_rec_name ^ " =\n\