src/HOL/Tools/BNF/bnf_lfp.ML

           end;
 
         val (Ibnf_consts, lthy) =
           fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
               fn T => fn lthy =>
-            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads)
+            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads)
               map_b rel_b set_bs
               ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
           bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
 
         val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts;

         fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN
           mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
           fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy =>
-            bnf_def Do_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
+            bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
               map_b rel_b set_bs consts lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           bs tacss map_bs rel_bs set_bss
             ((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels)
             lthy;