src/HOL/thy_syntax.ML
changeset 11628 e57a6e51715e
parent 9857 2f994c499bef
child 11804 d69e7acd9380
--- 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\