# HG changeset patch
# User blanchet
# Date 1348646459 -7200
# Node ID 040cfb087b3a9320bcca4a0f0bf0ee80b73d9919
# Parent  1c73b107d20d0c436bf60b9e8cade8177d745eea
leave out some internal theorems unless "bnf_note_all" is set

diff -r 1c73b107d20d -r 040cfb087b3a src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 03:16:40 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -59,6 +59,8 @@
   let
     val timer = time (Timer.startRealTimer ());
 
+    val note_all = Config.get lthy bnf_note_all;
+
     val live = live_of_bnf (hd bnfs);
     val n = length bnfs; (*active*)
     val ks = 1 upto n;
@@ -2945,8 +2947,11 @@
           [(dtor_mapN, map single folded_dtor_map_thms),
           (dtor_relN, map single dtor_Jrel_thms),
           (dtor_set_inclN, dtor_set_incl_thmss),
-          (dtor_set_set_inclN, map flat dtor_set_set_incl_thmsss),
-          (dtor_srelN, map single dtor_Jsrel_thms)] @
+          (dtor_set_set_inclN, map flat dtor_set_set_incl_thmsss)] @
+          (if note_all then
+             [(dtor_srelN, map single dtor_Jsrel_thms)]
+           else
+             []) @
           map2 (fn i => fn thms => (mk_dtor_setsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
@@ -2957,19 +2962,22 @@
       end;
 
       val common_notes =
-        [(dtor_coinductN, [dtor_coinduct_thm]),
-        (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
-        (dtor_rel_coinductN, [dtor_rel_coinduct_thm]),
-        (dtor_rel_strong_coinductN, [dtor_rel_strong_coinduct_thm]),
-        (dtor_srel_coinductN, [dtor_srel_coinduct_thm]),
-        (dtor_srel_strong_coinductN, [dtor_srel_strong_coinduct_thm])]
+        [(dtor_rel_coinductN, [dtor_rel_coinduct_thm]),
+        (dtor_rel_strong_coinductN, [dtor_rel_strong_coinduct_thm])] @
+        (if note_all then
+           [(dtor_coinductN, [dtor_coinduct_thm]),
+           (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
+           (dtor_srel_coinductN, [dtor_srel_coinduct_thm]),
+           (dtor_srel_strong_coinductN, [dtor_srel_strong_coinduct_thm])]
+         else
+           [])
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
       val notes =
         [(ctor_dtorN, ctor_dtor_thms),
+        (ctor_dtor_corecsN, ctor_dtor_corec_thms),
         (ctor_dtor_unfoldsN, ctor_dtor_unfold_thms),
-        (ctor_dtor_corecsN, ctor_dtor_corec_thms),
         (ctor_exhaustN, ctor_exhaust_thms),
         (ctor_injectN, ctor_inject_thms),
         (dtor_corecsN, dtor_corec_thms),
diff -r 1c73b107d20d -r 040cfb087b3a src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Sep 26 03:16:40 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -29,6 +29,9 @@
 fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
+
+    val note_all = Config.get lthy bnf_note_all;
+
     val live = live_of_bnf (hd bnfs);
     val n = length bnfs; (*active*)
     val ks = 1 upto n;
@@ -1785,8 +1788,11 @@
           [(ctor_mapN, map single folded_ctor_map_thms),
           (ctor_relN, map single ctor_Irel_thms),
           (ctor_set_inclN, ctor_set_incl_thmss),
-          (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss),
-          (ctor_srelN, map single ctor_Isrel_thms)] @
+          (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @
+          (if note_all then
+             [(ctor_srelN, map single ctor_Isrel_thms)]
+           else
+             []) @
           map2 (fn i => fn thms => (mk_ctor_setsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>