# HG changeset patch
# User blanchet
# Date 1379527079 -7200
# Node ID 657c89169d1a8c2da9b35de979251ea2de37d375
# Parent  0c565fec9c78a57f15b0af2fcca8daaf0b531c17
include more "discI" rules

diff -r 0c565fec9c78 -r 657c89169d1a src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 18 18:57:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 18 19:57:59 2013 +0200
@@ -518,23 +518,23 @@
               ks goals inject_thmss distinct_thmsss
           end;
 
-        val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
-             disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
+        val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
+             disc_exclude_thms, disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
           if no_discs_sels then
-            ([], [], [], [], [], [], [], [], [], [])
+            ([], [], [], [], [], [], [], [], [], [], [])
           else
             let
               fun make_sel_thm xs' case_thm sel_def =
                 zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
                     (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
 
+              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
+
               fun has_undefined_rhs thm =
                 (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
                   Const (@{const_name undefined}, _) => true
                 | _ => false);
 
-              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
-
               val all_sel_thms =
                 (if all_sels_distinct andalso forall null sel_defaultss then
                    flat sel_thmss
@@ -593,8 +593,16 @@
                   map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
                 end;
 
-              val disc_thms = flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
-                disc_bindings disc_thmss);
+              val nontriv_disc_thms =
+                flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
+                  disc_bindings disc_thmss);
+
+              fun is_discI_boring b =
+                (n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding);
+
+              val nontriv_discI_thms =
+                flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings
+                  discI_thms);
 
               val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
                 let
@@ -693,12 +701,11 @@
                   |> Proof_Context.export names_lthy lthy
                 end;
             in
-              (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
-               [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms)
+              (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
+               nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], collapse_thms,
+               expand_thms, case_conv_thms)
             end;
 
-        val nontriv_discI_thms = if n = 1 then [] else discI_thms;
-
         val (case_cong_thm, weak_case_cong_thm) =
           let
             fun mk_prem xctr xs xf xg =
@@ -753,7 +760,7 @@
            (case_congN, [case_cong_thm], []),
            (case_convN, case_conv_thms, []),
            (collapseN, collapse_thms, simp_attrs),
-           (discN, disc_thms, simp_attrs),
+           (discN, nontriv_disc_thms, simp_attrs),
            (discIN, nontriv_discI_thms, []),
            (disc_excludeN, disc_exclude_thms, []),
            (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),