--- a/src/HOL/Tools/inductive_package.ML Mon Nov 12 23:26:18 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML Mon Nov 12 23:27:04 2001 +0100
@@ -781,8 +781,9 @@
else
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
rec_sets_defs thy1;
- val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
- else standard (raw_induct RSN (2, rev_mp));
+ val induct =
+ if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0])
+ else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]);
val (thy2, intrs') =
thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
@@ -792,9 +793,8 @@
[(("intros", intrs'), []),
(("elims", elims), [RuleCases.consumes 1])]
|>>> PureThy.add_thms
- [((coind_prefix coind ^ "induct", rulify induct),
- [RuleCases.case_names induct_cases,
- RuleCases.consumes 1])]
+ [((coind_prefix coind ^ "induct", rulify (#1 induct)),
+ (RuleCases.case_names induct_cases :: #2 induct))]
|>> Theory.parent_path;
in (thy3,
{defs = fp_def :: rec_sets_defs,