src/HOL/Codatatype/Tools/bnf_def.ML

   val no_reflexive: thm list -> thm list
   val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
 
   datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
   datatype fact_policy =
-    Derive_Some_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms
+    Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms
   val bnf_note_all: bool Config.T
   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) ->

 val set_bdN = "set_bd";
 
 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
 
 datatype fact_policy =
-  Derive_Some_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms;
+  Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms;
 
 val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
 
 fun user_policy policy ctxt =
   if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else policy;

           Type (C, Ts) => if forall (is_some o try dest_TFree) Ts
             then (Binding.qualified_name C, C) else err bd_rhsT
         | T => err T)
       else (b, Local_Theory.full_name no_defs_lthy b);
 
-    fun maybe_define (b, rhs) lthy =
+    fun maybe_define needed_for_extra_facts (b, rhs) lthy =
       let
         val inline =
+          (not needed_for_extra_facts orelse fact_policy = Derive_Few_Facts) andalso
           (case const_policy of
             Dont_Inline => false
           | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
           | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_size
           | Do_Inline => true)

     val (((((bnf_map_term, raw_map_def),
       (bnf_set_terms, raw_set_defs)),
       (bnf_bd_term, raw_bd_def)),
       (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
         no_defs_lthy
-        |> maybe_define map_bind_def
-        ||>> apfst split_list o fold_map maybe_define set_binds_defs
-        ||>> maybe_define bd_bind_def
-        ||>> apfst split_list o fold_map maybe_define wit_binds_defs
+        |> maybe_define false map_bind_def
+        ||>> apfst split_list o fold_map (maybe_define false) set_binds_defs
+        ||>> maybe_define false bd_bind_def
+        ||>> apfst split_list o fold_map (maybe_define false) wit_binds_defs
         ||> `(maybe_restore no_defs_lthy);
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val bnf_map_def = Morphism.thm phi raw_map_def;

 
     val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
 
     val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) =
       lthy
-      |> maybe_define rel_bind_def
+      |> maybe_define false rel_bind_def
       ||> `(maybe_restore lthy);
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val bnf_rel_def = Morphism.thm phi raw_rel_def;
     val bnf_rel = Morphism.term phi bnf_rel_term;

         Qs As' Bs')));
     val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs);
 
     val ((bnf_pred_term, raw_pred_def), (lthy, lthy_old)) =
       lthy
-      |> maybe_define pred_bind_def
+      |> maybe_define true pred_bind_def
       ||> `(maybe_restore lthy);
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val bnf_pred_def = Morphism.thm phi raw_pred_def;
     val bnf_pred = Morphism.term phi bnf_pred_term;

 
         val bd_Card_order = #bd_card_order axioms RS @{thm conjunct2[OF card_order_on_Card_order]};
         val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order];
         val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
 
-        fun mk_lazy f = if fact_policy <> Derive_Some_Facts then Lazy.value (f ()) else Lazy.lazy f;
+        fun mk_lazy f = if fact_policy <> Derive_Few_Facts then Lazy.value (f ()) else Lazy.lazy f;
 
         fun mk_collect_set_natural () =
           let
             val defT = mk_bnf_T Ts CA --> HOLogic.mk_setT T;
             val collect_map = HOLogic.mk_comp