# HG changeset patch
# User blanchet
# Date 1380048762 -7200
# Node ID a1632a5f5fb300b062305486afe49a98c8fd68d0
# Parent  687116951569299cba99c77837710173120eaf81
added [dest] to "disc_exclude"

diff -r 687116951569 -r a1632a5f5fb3 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Tue Sep 24 20:40:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Tue Sep 24 20:52:42 2013 +0200
@@ -129,6 +129,7 @@
 val weak_case_cong_thmsN = "weak_case_cong";
 
 val cong_attrs = @{attributes [cong]};
+val dest_attrs = @{attributes [dest]};
 val safe_elim_attrs = @{attributes [elim!]};
 val iff_attrs = @{attributes [iff]};
 val induct_simp_attrs = @{attributes [induct_simp]};
@@ -766,7 +767,7 @@
            (collapseN, safe_collapse_thms, simp_attrs),
            (discN, nontriv_disc_thms, simp_attrs),
            (discIN, nontriv_discI_thms, []),
-           (disc_excludeN, disc_exclude_thms, []),
+           (disc_excludeN, disc_exclude_thms, dest_attrs),
            (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
            (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
            (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),