mutual rules declared as ``consumes 0'';
authorwenzelm
Mon Nov 12 23:27:04 2001 +0100 (2001-11-12 ago)
changeset 1216514e94ad99861
parent 12164 0b219d9e3384
child 12166 5fc22b8c03e9
mutual rules declared as ``consumes 0'';
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Nov 12 23:26:18 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Nov 12 23:27:04 2001 +0100
     1.3 @@ -781,8 +781,9 @@
     1.4        else
     1.5          prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
     1.6            rec_sets_defs thy1;
     1.7 -    val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
     1.8 -      else standard (raw_induct RSN (2, rev_mp));
     1.9 +    val induct =
    1.10 +      if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0])
    1.11 +      else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]);
    1.12  
    1.13      val (thy2, intrs') =
    1.14        thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
    1.15 @@ -792,9 +793,8 @@
    1.16          [(("intros", intrs'), []),
    1.17            (("elims", elims), [RuleCases.consumes 1])]
    1.18        |>>> PureThy.add_thms
    1.19 -        [((coind_prefix coind ^ "induct", rulify induct),
    1.20 -         [RuleCases.case_names induct_cases,
    1.21 -          RuleCases.consumes 1])]
    1.22 +        [((coind_prefix coind ^ "induct", rulify (#1 induct)),
    1.23 +         (RuleCases.case_names induct_cases :: #2 induct))]
    1.24        |>> Theory.parent_path;
    1.25    in (thy3,
    1.26      {defs = fp_def :: rec_sets_defs,