1.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 18 18:12:40 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 18 18:53:24 2013 +0200
     1.3 @@ -116,6 +116,7 @@
     1.4  val disc_excludeN = "disc_exclude";
     1.5  val disc_exhaustN = "disc_exhaust";
     1.6  val discN = "disc";
     1.7 +val discIN = "discI";
     1.8  val distinctN = "distinct";
     1.9  val exhaustN = "exhaust";
    1.10  val expandN = "expand";
    1.11 @@ -127,10 +128,10 @@
    1.12  val split_asmN = "split_asm";
    1.13  val weak_case_cong_thmsN = "weak_case_cong";
    1.14  
    1.15 +val cong_attrs = @{attributes [cong]};
    1.16 +val safe_elim_attrs = @{attributes [elim!]};
    1.17 +val iff_attrs = @{attributes [iff]};
    1.18  val induct_simp_attrs = @{attributes [induct_simp]};
    1.19 -val cong_attrs = @{attributes [cong]};
    1.20 -val iff_attrs = @{attributes [iff]};
    1.21 -val safe_elim_attrs = @{attributes [elim!]};
    1.22  val simp_attrs = @{attributes [simp]};
    1.23  
    1.24  fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
    1.25 @@ -696,6 +697,8 @@
    1.26                 [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms)
    1.27              end;
    1.28  
    1.29 +        val nontriv_discI_thms = if n = 1 then [] else discI_thms;
    1.30 +
    1.31          val (case_cong_thm, weak_case_cong_thm) =
    1.32            let
    1.33              fun mk_prem xctr xs xf xg =
    1.34 @@ -751,6 +754,7 @@
    1.35             (case_convN, case_conv_thms, []),
    1.36             (collapseN, collapse_thms, simp_attrs),
    1.37             (discN, disc_thms, simp_attrs),
    1.38 +           (discIN, nontriv_discI_thms, []),
    1.39             (disc_excludeN, disc_exclude_thms, []),
    1.40             (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
    1.41             (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),