# HG changeset patch
# User blanchet
# Date 1379523204 -7200
# Node ID e6a44d775be396a89b2156cad6fea370c6a81808
# Parent  7d32f33d340d141e40944a3f6b8fc274021468ae
note "discI"

diff -r 7d32f33d340d -r e6a44d775be3 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 18 18:12:40 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 18 18:53:24 2013 +0200
@@ -116,6 +116,7 @@
 val disc_excludeN = "disc_exclude";
 val disc_exhaustN = "disc_exhaust";
 val discN = "disc";
+val discIN = "discI";
 val distinctN = "distinct";
 val exhaustN = "exhaust";
 val expandN = "expand";
@@ -127,10 +128,10 @@
 val split_asmN = "split_asm";
 val weak_case_cong_thmsN = "weak_case_cong";
 
+val cong_attrs = @{attributes [cong]};
+val safe_elim_attrs = @{attributes [elim!]};
+val iff_attrs = @{attributes [iff]};
 val induct_simp_attrs = @{attributes [induct_simp]};
-val cong_attrs = @{attributes [cong]};
-val iff_attrs = @{attributes [iff]};
-val safe_elim_attrs = @{attributes [elim!]};
 val simp_attrs = @{attributes [simp]};
 
 fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
@@ -696,6 +697,8 @@
                [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 =
@@ -751,6 +754,7 @@
            (case_convN, case_conv_thms, []),
            (collapseN, collapse_thms, simp_attrs),
            (discN, disc_thms, simp_attrs),
+           (discIN, nontriv_discI_thms, []),
            (disc_excludeN, disc_exclude_thms, []),
            (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
            (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),