# HG changeset patch
# User desharna
# Date 1411734909 -7200
# Node ID 8bdcff16124de1918df5f6903566d885e0e89ddc
# Parent  126c353540fc081be30ce08a10c14f9d8da332f6
add attribute 'case_names' to 'set_case'

diff -r 126c353540fc -r 8bdcff16124d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 09:58:35 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 14:35:09 2014 +0200
@@ -600,9 +600,13 @@
               val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
               val cases_set_attr =
                 Attrib.internal (K (Induct.cases_pred (name_of_set set)));
+
+              val ctr_names = quasi_unambiguous_case_names (flat
+                (map (uncurry mk_names o map_prod length name_of_ctr) (premss ~~ ctrAs)));
+              val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names));
             in
               (* TODO: @{attributes [elim?]} *)
-              (thm, [consumes_attr, cases_set_attr])
+              (thm, [consumes_attr, cases_set_attr, case_names_attr])
             end) setAs)
         end;