src/HOL/Tools/inductive_package.ML
changeset 5108 4074c7d86d44
parent 5094 ddcc3c114a0e
child 5120 f7f5442c934a
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jul 01 18:43:40 1998 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Jul 01 19:03:54 1998 +0200
     1.3 @@ -454,7 +454,7 @@
     1.4        else
     1.5          prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
     1.6            rec_sets_defs thy';
     1.7 -    val induct = if coind orelse length cs > 1 then raw_induct
     1.8 +    val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
     1.9        else standard (raw_induct RSN (2, rev_mp));
    1.10  
    1.11      val thy'' = thy' |>