# HG changeset patch
# User blanchet
# Date 1382101082 -7200
# Node ID 71dc4e6c001ca2102ccd3f726908a1baa75f4e13
# Parent  942bb9d9b7a8e3e58afd16f03b8d5c7cc9d08ecf
set code attribute on discriminator equations

diff -r 942bb9d9b7a8 -r 71dc4e6c001c src/HOL/BNF/Tools/ctr_sugar.ML
--- a/src/HOL/BNF/Tools/ctr_sugar.ML	Fri Oct 18 13:38:55 2013 +0200
+++ b/src/HOL/BNF/Tools/ctr_sugar.ML	Fri Oct 18 14:58:02 2013 +0200
@@ -177,7 +177,8 @@
 val inductsimp_attrs = @{attributes [induct_simp]};
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
-val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
+val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
+val code_nitpicksimp_simp_attrs = code_nitpicksimp_attrs @ simp_attrs;
 
 fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
 
@@ -869,6 +870,13 @@
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
         val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
 
+        val anonymous_notes =
+          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
+           (map (fn th => th RS @{thm eq_False[THEN iffD2]}
+              handle THM _ => th RS @{thm eq_True[THEN iffD2]}) nontriv_disc_thms,
+            code_nitpicksimp_attrs)]
+          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
         val notes =
           [(caseN, case_thms, code_nitpicksimp_simp_attrs),
            (case_congN, [case_cong_thm], []),
@@ -895,10 +903,6 @@
           |> map (fn (thmN, thms, attrs) =>
             ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
 
-        val anonymous_notes =
-          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
-          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
-
         val ctr_sugar =
           {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
            nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,