diff -r a7701b1d6c6a -r e8346dad78e1 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Dec 01 19:42:35 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 01 19:43:06 2000 +0100
@@ -796,7 +796,7 @@
     val induct_cases = map (#1 o #1) intros;
 
     val (thy1, result as {elims, induct, ...}) =
-      (if ! quick_and_dirty then add_ind_axm else add_ind_def)
+      (if ! quick_and_dirty andalso not coind (* FIXME *) then add_ind_axm else add_ind_def)
         verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
         con_defs thy params paramTs cTs cnames induct_cases;
     val thy2 = thy1