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

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 09:15:53 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 18 11:06:25 2012 +0200
     2.3 @@ -82,7 +82,7 @@
     2.4    datatype fact_policy =
     2.5      Derive_Some_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms
     2.6    val bnf_note_all: bool Config.T
     2.7 -  val user_policy: Proof.context -> fact_policy
     2.8 +  val user_policy: fact_policy -> Proof.context -> fact_policy
     2.9  
    2.10    val print_bnfs: Proof.context -> unit
    2.11    val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
    2.12 @@ -505,8 +505,8 @@
    2.13  
    2.14  val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
    2.15  
    2.16 -fun user_policy ctxt =
    2.17 -  if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else Derive_All_Facts_Note_Most;
    2.18 +fun user_policy policy ctxt =
    2.19 +  if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else policy;
    2.20  
    2.21  val smart_max_inline_size = 25; (*FUDGE*)
    2.22  
    2.23 @@ -1193,7 +1193,7 @@
    2.24    Proof.unfolding ([[(defs, [])]])
    2.25      (Proof.theorem NONE (snd o register_bnf key oo after_qed)
    2.26        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
    2.27 -  prepare_def Do_Inline user_policy I Syntax.read_term NONE;
    2.28 +  prepare_def Do_Inline (user_policy Derive_All_Facts_Note_Most) I Syntax.read_term NONE;
    2.29  
    2.30  fun print_bnfs ctxt =
    2.31    let

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

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