--- a/src/HOL/thy_syntax.ML Fri Sep 28 19:18:46 2001 +0200
+++ b/src/HOL/thy_syntax.ML Fri Sep 28 19:19:26 2001 +0200
@@ -63,7 +63,7 @@
\local\n\
\val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
\ InductivePackage.add_inductive true " ^
- (if coind then "true " else "false ") ^ srec_tms ^ " [] " ^
+ (if coind then "true " else "false ") ^ srec_tms ^
sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
\in\n\
\structure " ^ big_rec_name ^ " =\n\