src/HOL/Tools/inductive.ML
changeset 50771 2852f997bfb5
parent 50302 9149a07a6c67
child 51551 88d1d19fb74f
     1.1 --- a/src/HOL/Tools/inductive.ML	Tue Jan 08 13:24:12 2013 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Tue Jan 08 16:01:07 2013 +0100
     1.3 @@ -860,12 +860,17 @@
     1.4      val ind_case_names = Rule_Cases.case_names intr_names;
     1.5      val induct =
     1.6        if coind then
     1.7 -        (raw_induct, [Rule_Cases.case_names [rec_name],
     1.8 +        (raw_induct,
     1.9 +         [Rule_Cases.case_names [rec_name],
    1.10            Rule_Cases.case_conclusion (rec_name, intr_names),
    1.11 -          Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)])
    1.12 +          Rule_Cases.consumes (1 - Thm.nprems_of raw_induct),
    1.13 +          Induct.coinduct_pred (hd cnames)])
    1.14        else if no_ind orelse length cnames > 1 then
    1.15 -        (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
    1.16 -      else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
    1.17 +        (raw_induct,
    1.18 +          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))])
    1.19 +      else
    1.20 +        (raw_induct RSN (2, rev_mp),
    1.21 +          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]);
    1.22  
    1.23      val (intrs', lthy1) =
    1.24        lthy |>
    1.25 @@ -883,7 +888,7 @@
    1.26          Local_Theory.note
    1.27            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
    1.28              [Attrib.internal (K (Rule_Cases.case_names cases)),
    1.29 -             Attrib.internal (K (Rule_Cases.consumes 1)),
    1.30 +             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim))),
    1.31               Attrib.internal (K (Rule_Cases.constraints k)),
    1.32               Attrib.internal (K (Induct.cases_pred name)),
    1.33               Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
    1.34 @@ -906,7 +911,7 @@
    1.35            Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
    1.36              inducts |> map (fn (name, th) => ([th],
    1.37                [Attrib.internal (K ind_case_names),
    1.38 -               Attrib.internal (K (Rule_Cases.consumes 1)),
    1.39 +               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
    1.40                 Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
    1.41          end;
    1.42    in (intrs', elims', eqs', induct', inducts, lthy4) end;