# HG changeset patch
# User wenzelm
# Date 1005604024 -3600
# Node ID 14e94ad99861aed3880147b883a031eefb52f1bf
# Parent  0b219d9e3384b9943c7c099b67e8c4d0f5623a79
mutual rules declared as ``consumes 0'';

diff -r 0b219d9e3384 -r 14e94ad99861 src/HOL/Tools/inductive_package.ML
--- 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,