# HG changeset patch
# User wenzelm
# Date 975696186 -3600
# Node ID e8346dad78e1d5201fff701fb830dc83319fb019
# Parent  a7701b1d6c6a4e75b26c21bbd4912fc472820762
ignore quick_and_dirty for coind;

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