--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Aug 18 18:48:39 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Aug 18 19:16:30 2014 +0200
@@ -1574,9 +1574,13 @@
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
|> rotate_prems ~1;
+
+ val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
+ val cases_set_attr =
+ Attrib.internal (K (Induct.cases_pred (name_of_set set)));
in
- (thm, [](* TODO: [@{attributes [elim?]},
- Attrib.internal (K (Induct.cases_pred (name_of_set set)))] *))
+ (* TODO: @{attributes [elim?]} *)
+ (thm, [consumes_attr, cases_set_attr])
end) setAs)
end;