prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');

--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Jan 08 13:24:12 2013 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Jan 08 16:01:07 2013 +0100
@@ -540,7 +540,7 @@
 
   in
     ctxt'' |>
-    Proof.theorem NONE (fn thss => fn ctxt =>
+    Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
@@ -553,27 +553,27 @@
           mk_ind_proof ctxt thss' |> Inductive.rulify;
         val strong_cases = map (mk_cases_proof ##> Inductive.rulify)
           (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
+        val strong_induct_atts =
+          map (Attrib.internal o K)
+            [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
         val strong_induct =
-          if length names > 1 then
-            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
-          else (strong_raw_induct RSN (2, rev_mp),
-            [ind_case_names, Rule_Cases.consumes 1]);
+          if length names > 1 then strong_raw_induct
+          else strong_raw_induct RSN (2, rev_mp);
         val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
-          ((rec_qualified (Binding.name "strong_induct"),
-            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
+          ((rec_qualified (Binding.name "strong_induct"), strong_induct_atts), [strong_induct]);
         val strong_inducts =
           Project_Rule.projects ctxt (1 upto length names) strong_induct';
       in
         ctxt' |>
-        Local_Theory.note
-          ((rec_qualified (Binding.name "strong_inducts"),
-            [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (Rule_Cases.consumes 1))]),
-           strong_inducts) |> snd |>
+        Local_Theory.notes
+          [((rec_qualified (Binding.name "strong_inducts"), []),
+            strong_inducts |> map (fn th => ([th],
+              [Attrib.internal (K ind_case_names),
+               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd |>
         Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
             ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
               [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
-               Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
+               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim)))]), [([elim], [])]))
           (strong_cases ~~ induct_cases')) |> snd
       end)
       (map (map (rulify_term thy #> rpair [])) vc_compat)

--- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Jan 08 13:24:12 2013 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Jan 08 16:01:07 2013 +0100
@@ -443,7 +443,7 @@
 
   in
     ctxt'' |>
-    Proof.theorem NONE (fn thss => fn ctxt =>
+    Proof.theorem NONE (fn thss => fn ctxt =>  (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
@@ -454,28 +454,27 @@
         val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
         val strong_raw_induct =
           mk_ind_proof ctxt thss' |> Inductive.rulify;
+        val strong_induct_atts =
+          map (Attrib.internal o K)
+            [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
         val strong_induct =
-          if length names > 1 then
-            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
-          else (strong_raw_induct RSN (2, rev_mp),
-            [ind_case_names, Rule_Cases.consumes 1]);
+          if length names > 1 then strong_raw_induct
+          else strong_raw_induct RSN (2, rev_mp);
         val (induct_name, inducts_name) =
           case alt_name of
             NONE => (rec_qualified (Binding.name "strong_induct"),
                      rec_qualified (Binding.name "strong_inducts"))
           | SOME s => (Binding.name s, Binding.name (s ^ "s"));
         val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
-          ((induct_name,
-            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
+          ((induct_name, strong_induct_atts), [strong_induct]);
         val strong_inducts =
           Project_Rule.projects ctxt' (1 upto length names) strong_induct'
       in
         ctxt' |>
-        Local_Theory.note
-          ((inducts_name,
+        Local_Theory.notes [((inducts_name, []),
+          strong_inducts |> map (fn th => ([th],
             [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (Rule_Cases.consumes 1))]),
-           strong_inducts) |> snd
+             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
       end)
       (map (map (rulify_term thy #> rpair [])) vc_compat)
   end;

--- a/src/HOL/Tools/Function/function.ML	Tue Jan 08 13:24:12 2013 +0100
+++ b/src/HOL/Tools/Function/function.ML	Tue Jan 08 16:01:07 2013 +0100
@@ -105,14 +105,15 @@
 
         val addsmps = add_simps fnames post sort_cont
 
-        val (((psimps', pinducts'), (_, [termination'])), lthy) =
+        val (((psimps', [pinducts']), (_, [termination'])), lthy) =
           lthy
           |> addsmps (conceal_partial o Binding.qualify false "partial")
                "psimps" conceal_partial psimp_attribs psimps
-          ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
+          ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
+                simple_pinducts |> map (fn th => ([th],
                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
-                  Attrib.internal (K (Rule_Cases.consumes 1)),
-                  Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
+                  Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
+                  Attrib.internal (K (Induct.induct_pred ""))])))]
           ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
           ||> (snd o Local_Theory.note ((qualify "cases",
                  [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))

--- a/src/HOL/Tools/inductive.ML	Tue Jan 08 13:24:12 2013 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Jan 08 16:01:07 2013 +0100
@@ -860,12 +860,17 @@
     val ind_case_names = Rule_Cases.case_names intr_names;
     val induct =
       if coind then
-        (raw_induct, [Rule_Cases.case_names [rec_name],
+        (raw_induct,
+         [Rule_Cases.case_names [rec_name],
           Rule_Cases.case_conclusion (rec_name, intr_names),
-          Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)])
+          Rule_Cases.consumes (1 - Thm.nprems_of raw_induct),
+          Induct.coinduct_pred (hd cnames)])
       else if no_ind orelse length cnames > 1 then
-        (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
-      else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
+        (raw_induct,
+          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))])
+      else
+        (raw_induct RSN (2, rev_mp),
+          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]);
 
     val (intrs', lthy1) =
       lthy |>
@@ -883,7 +888,7 @@
         Local_Theory.note
           ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
             [Attrib.internal (K (Rule_Cases.case_names cases)),
-             Attrib.internal (K (Rule_Cases.consumes 1)),
+             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim))),
              Attrib.internal (K (Rule_Cases.constraints k)),
              Attrib.internal (K (Induct.cases_pred name)),
              Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
@@ -906,7 +911,7 @@
           Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
             inducts |> map (fn (name, th) => ([th],
               [Attrib.internal (K ind_case_names),
-               Attrib.internal (K (Rule_Cases.consumes 1)),
+               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
                Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
         end;
   in (intrs', elims', eqs', induct', inducts, lthy4) end;