# HG changeset patch
# User blanchet
# Date 1408433670 -7200
# Node ID f50b3726266f3fe4eaa88e9bb144797b0f5e18b6
# Parent  90d941a477bd82f4849006fb59ec7d703d4d54c4
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set

diff -r 90d941a477bd -r f50b3726266f src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
--- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Tue Aug 19 09:34:27 2014 +0200
+++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Tue Aug 19 09:34:30 2014 +0200
@@ -47,13 +47,13 @@
 using Node unfolding Node_def
 by (metis Node Node_root_cont finite_cont)
 
-lemma dtree_sel_ctor[simp]:
+lemma dtree_sel_ctr[simp]:
 "root (Node n as) = n"
 "finite as \<Longrightarrow> cont (Node n as) = as"
 unfolding Node_def cont_def by auto
 
-lemmas root_Node = dtree_sel_ctor(1)
-lemmas cont_Node = dtree_sel_ctor(2)
+lemmas root_Node = dtree_sel_ctr(1)
+lemmas cont_Node = dtree_sel_ctr(2)
 
 lemma dtree_cong:
 assumes "root tr = root tr'" and "cont tr = cont tr'"
diff -r 90d941a477bd -r f50b3726266f src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Tue Aug 19 09:34:27 2014 +0200
+++ b/src/HOL/BNF_GFP.thy	Tue Aug 19 09:34:30 2014 +0200
@@ -285,12 +285,12 @@
 qed
 
 lemma univ_preserves:
-  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall> x \<in> A. f x \<in> B"
+  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
   shows "\<forall>X \<in> A//r. univ f X \<in> B"
 proof
   fix X assume "X \<in> A//r"
   then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
-  hence "univ f X = f x" using assms univ_commute by fastforce
+  hence "univ f X = f x" using ECH RES univ_commute by fastforce
   thus "univ f X \<in> B" using x PRES by simp
 qed
 
diff -r 90d941a477bd -r f50b3726266f src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Aug 19 09:34:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Aug 19 09:34:30 2014 +0200
@@ -2514,12 +2514,7 @@
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
         bs thmss);
 
-    (*FIXME: once the package exports all the necessary high-level characteristic theorems,
-       those should not only be concealed but rather not noted at all*)
-    val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
-
-    val (noted, lthy') =
-      lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes));
+    val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
 
     val fp_res =
       {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs,
@@ -2528,8 +2523,7 @@
        xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
        xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
        xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
-       dtor_set_induct_thms = dtor_Jset_induct_thms}
-      |> morph_fp_result (substitute_noted_thm noted);
+       dtor_set_induct_thms = dtor_Jset_induct_thms};
   in
     timer; (fp_res, lthy')
   end;
diff -r 90d941a477bd -r f50b3726266f src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Aug 19 09:34:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Aug 19 09:34:30 2014 +0200
@@ -1801,12 +1801,7 @@
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
         bs thmss);
 
-    (*FIXME: once the package exports all the necessary high-level characteristic theorems,
-       those should not only be concealed but rather not noted at all*)
-    val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
-
-    val (noted, lthy') =
-      lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes));
+    val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes);
 
     val fp_res =
       {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs,
@@ -1815,8 +1810,7 @@
        xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
        xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
        xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
-       dtor_set_induct_thms = []}
-      |> morph_fp_result (substitute_noted_thm noted);
+       dtor_set_induct_thms = []};
   in
     timer; (fp_res, lthy')
   end;