src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 57987 ecb227b40907
parent 57983 6edc3529bb4e
child 57999 412ec967e3b3
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 18:48:39 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 19:16:30 2014 +0200
     1.3 @@ -1574,9 +1574,13 @@
     1.4                              |> singleton (Proof_Context.export names_lthy lthy)
     1.5                              |> Thm.close_derivation
     1.6                              |> rotate_prems ~1;
     1.7 +
     1.8 +                          val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
     1.9 +                          val cases_set_attr =
    1.10 +                            Attrib.internal (K (Induct.cases_pred (name_of_set set)));
    1.11                          in
    1.12 -                          (thm, [](* TODO: [@{attributes [elim?]},
    1.13 -                            Attrib.internal (K (Induct.cases_pred (name_of_set set)))] *))
    1.14 +                          (* TODO: @{attributes [elim?]} *)
    1.15 +                          (thm, [consumes_attr, cases_set_attr])
    1.16                          end) setAs)
    1.17                      end;
    1.18