# HG changeset patch # User berghofe # Date 899312634 -7200 # Node ID 4074c7d86d44cb0a7a57e90d8cefffad8aedd0d5 # Parent 2edf5dfb02f322f6e0aa062c753d5d4dd38cabe0 Fixed bug (improper handling of flag no_ind). diff -r 2edf5dfb02f3 -r 4074c7d86d44 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Wed Jul 01 18:43:40 1998 +0200 +++ b/src/HOL/Tools/inductive_package.ML Wed Jul 01 19:03:54 1998 +0200 @@ -454,7 +454,7 @@ else prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def rec_sets_defs thy'; - val induct = if coind orelse length cs > 1 then raw_induct + val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct else standard (raw_induct RSN (2, rev_mp)); val thy'' = thy' |>