bnf_note_all mode for "pre_"-BNFs

--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Tue Sep 18 09:15:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Tue Sep 18 11:06:25 2012 +0200
@@ -677,7 +677,9 @@
 
     fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
 
-    val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac (SOME deads)
+    val policy = user_policy Derive_All_Facts;
+
+    val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
       ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
 
     val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');

--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 09:15:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 11:06:25 2012 +0200
@@ -82,7 +82,7 @@
   datatype fact_policy =
     Derive_Some_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms
   val bnf_note_all: bool Config.T
-  val user_policy: Proof.context -> fact_policy
+  val user_policy: fact_policy -> Proof.context -> fact_policy
 
   val print_bnfs: Proof.context -> unit
   val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
@@ -505,8 +505,8 @@
 
 val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
 
-fun user_policy ctxt =
-  if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else Derive_All_Facts_Note_Most;
+fun user_policy policy ctxt =
+  if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else policy;
 
 val smart_max_inline_size = 25; (*FUDGE*)
 
@@ -1193,7 +1193,7 @@
   Proof.unfolding ([[(defs, [])]])
     (Proof.theorem NONE (snd o register_bnf key oo after_qed)
       (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
-  prepare_def Do_Inline user_policy I Syntax.read_term NONE;
+  prepare_def Do_Inline (user_policy Derive_All_Facts_Note_Most) I Syntax.read_term NONE;
 
 fun print_bnfs ctxt =
   let

--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 18 09:15:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 18 11:06:25 2012 +0200
@@ -2854,9 +2854,11 @@
 
         val wit_tac = mk_wit_tac n unf_fld_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
 
+        val policy = user_policy Derive_All_Facts_Note_Most;
+
         val (Jbnfs, lthy) =
           fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => fn lthy =>
-            bnf_def Dont_Inline user_policy I tacs (wit_tac thms) (SOME deads)
+            bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads)
               ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts all_witss lthy;

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 18 09:15:53 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 18 11:06:25 2012 +0200
@@ -1700,9 +1700,11 @@
 
         fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
 
+        val policy = user_policy Derive_All_Facts_Note_Most;
+
         val (Ibnfs, lthy) =
           fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => fn lthy =>
-            bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads)
+            bnf_def Dont_Inline policy I tacs wit_tac (SOME deads)
               ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;