unfold intermediate definitions after sealing the bnf

--- a/src/HOL/BNF_Comp.thy	Sun Mar 09 22:45:09 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Mon Mar 10 13:23:16 2014 +0100
@@ -147,6 +147,9 @@
 
 definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
 
+lemma id_bnf_comp_apply: "id_bnf_comp x = x"
+  unfolding id_bnf_comp_def by simp
+
 bnf ID: 'a
   map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   sets: "\<lambda>x. {x}"

--- a/src/HOL/Library/bnf_decl.ML	Sun Mar 09 22:45:09 2014 +0100
+++ b/src/HOL/Library/bnf_decl.ML	Mon Mar 10 13:23:16 2014 +0100
@@ -68,7 +68,7 @@
     val Fwits = map2 (fn witb => fn witT =>
       Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
     val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
-      prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads))
+      prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
       user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
       lthy;
 

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Mar 09 22:45:09 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 10 13:23:16 2014 +0100
@@ -338,8 +338,8 @@
         (maps wit_thms_of_bnf inners);
 
     val (bnf', lthy') =
-      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
-        Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
+      bnf_def const_policy (K Dont_Note) true qualify tacs wit_tac (SOME (oDs @ flat Dss))
+        Binding.empty Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
 
     val phi =
       Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def])
@@ -436,8 +436,8 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
-        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
+      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (killedAs @ Ds))
+        Binding.empty Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -526,8 +526,8 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
-        [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
+      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
+        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -607,8 +607,8 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
-        [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
+      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
+        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -765,21 +765,6 @@
       |> mk_Frees' "f" (map2 (curry op -->) As Bs)
       ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
 
-    val map_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#map_unfolds unfold_set);
-    val set_unfoldss = #set_unfoldss unfold_set;
-    val rel_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#rel_unfolds unfold_set);
-
-    val expand_maps = expand_id_bnf_comp_def o
-      fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
-    val expand_sets =
-      fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
-    val expand_rels = expand_id_bnf_comp_def o
-      fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
-    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: map_unfolds);
-    fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
-    fun unfold_rels ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: rel_unfolds);
-    fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
-
     val repTA = mk_T_of_bnf Ds As bnf;
     val T_bind = qualify b;
     val TA_params = Term.add_tfreesT repTA [];
@@ -800,12 +785,12 @@
       abs_inverse = Abs_inverse', type_definition = type_definition};
 
     val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB,
-      Term.list_comb (expand_maps (mk_map_of_bnf Ds As Bs bnf), fs)), RepA));
-    val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA)) o expand_maps o expand_sets)
+      Term.list_comb (mk_map_of_bnf Ds As Bs bnf, fs)), RepA));
+    val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA)))
       (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
     val bnf_bd = mk_bd_of_bnf Ds As bnf;
     val bnf_rel = fold_rev Term.absfree Rs' (mk_vimage2p RepA RepB $
-      (Term.list_comb (expand_rels (mk_rel_of_bnf Ds As Bs bnf), Rs)));
+      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, Rs)));
 
     (*bd may depend only on dead type variables*)
     val bd_repT = fst (dest_relT (fastype_of bnf_bd));
@@ -836,24 +821,22 @@
           (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite)
         end;
 
-    fun map_id0_tac ctxt =
-      rtac (@{thm type_copy_map_id0} OF [type_definition, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;
-    fun map_comp0_tac ctxt =
-      rtac (@{thm type_copy_map_comp0} OF
-        [type_definition, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1;
-    fun map_cong0_tac ctxt =
-      EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (unfold_all ctxt (map_cong0_of_bnf bnf)) ::
+    fun map_id0_tac _ =
+      rtac (@{thm type_copy_map_id0} OF [type_definition, map_id0_of_bnf bnf]) 1;
+    fun map_comp0_tac _ =
+      rtac (@{thm type_copy_map_comp0} OF [type_definition, map_comp0_of_bnf bnf]) 1;
+    fun map_cong0_tac _ =
+      EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (map_cong0_of_bnf bnf) ::
         map (fn i => EVERY' [select_prem_tac live (dtac meta_spec) i, etac meta_mp,
           etac (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
-    fun set_map0_tac thm ctxt =
-      rtac (@{thm type_copy_set_map0} OF [type_definition, unfold_all ctxt thm]) 1;
-    val set_bd_tacs = map (fn thm => fn ctxt => rtac (@{thm ordLeq_ordIso_trans} OF
-        [unfold_sets ctxt thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1)
-      (set_bd_of_bnf bnf);
-    fun le_rel_OO_tac ctxt =
-      rtac (unfold_rels ctxt (le_rel_OO_of_bnf bnf) RS @{thm vimage2p_relcompp_mono}) 1;
+    fun set_map0_tac thm _ =
+      rtac (@{thm type_copy_set_map0} OF [type_definition, thm]) 1;
+    val set_bd_tacs = map (fn thm => fn _ => rtac (@{thm ordLeq_ordIso_trans} OF
+        [thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) (set_bd_of_bnf bnf);
+    fun le_rel_OO_tac _ =
+      rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1;
     fun rel_OO_Grp_tac ctxt =
-      (rtac (unfold_all ctxt (rel_OO_Grp_of_bnf bnf) RS @{thm vimage2p_cong} RS trans) THEN'
+      (rtac (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN'
       SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
         type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
         type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
@@ -864,18 +847,40 @@
 
     val bnf_wits = map (fn (I, t) =>
         fold Term.absdummy (map (nth As) I)
-          (AbsA $ Term.list_comb (expand_id_bnf_comp_def t, map Bound (0 upto length I - 1))))
+          (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
       (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
-    fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
-      mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
+    fun wit_tac _ = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
+      mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME all_deads)
+      bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads)
         Binding.empty Binding.empty []
         ((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
+
+    val unfolds = @{thm id_bnf_comp_apply} ::
+      (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
+
+    val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
+    
+    val map_def = map_def_of_bnf bnf'';
+    val set_defs = set_defs_of_bnf bnf'';
+    val rel_def = map_def_of_bnf bnf'';
+
+    val bnf_b = qualify b;
+    val def_qualify =
+      Thm.def_binding o Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
+    fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
+    val map_b = def_qualify (mk_prefix_binding mapN);
+    val rel_b = def_qualify (mk_prefix_binding relN);
+    val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)]
+      else map (fn i => def_qualify (mk_prefix_binding (mk_setN i))) (1 upto live);
+
+    val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
+      |> map (fn (b, def) => ((b, []), [([def], [])]))
+    val lthy'' = lthy' |> Local_Theory.notes notes |> snd
   in
-    ((bnf', (all_deads, absT_info)), lthy')
+    ((bnf'', (all_deads, absT_info)), lthy'')
   end;
 
 exception BAD_DEAD of typ * typ;

--- a/src/HOL/Tools/BNF/bnf_def.ML	Sun Mar 09 22:45:09 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 10 13:23:16 2014 +0100
@@ -12,6 +12,7 @@
   type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
 
   val morph_bnf: morphism -> bnf -> bnf
+  val morph_bnf_defs: morphism -> bnf -> bnf
   val bnf_of: Proof.context -> string -> bnf option
   val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
 
@@ -100,16 +101,16 @@
     Proof.context
 
   val print_bnfs: Proof.context -> unit
-  val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
-    (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option ->
-    binding -> binding -> binding list ->
+  val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool ->
+    (binding -> binding) -> (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) ->
+    typ list option -> binding -> binding -> binding list ->
     (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
     string * term list *
     ((Proof.context -> thm list -> tactic) option * term list list) *
     ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
     local_theory * thm list
 
-  val define_bnf_consts: inline_policy -> fact_policy -> typ list option ->
+  val define_bnf_consts: inline_policy -> fact_policy -> bool -> typ list option ->
     binding -> binding -> binding list ->
     (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
       ((typ list * typ list * typ list * typ) *
@@ -121,7 +122,7 @@
         (typ list -> typ list -> typ list -> term) *
         (typ list -> typ list -> typ list -> term))) * local_theory
 
-  val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
+  val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> (binding -> binding) ->
     (Proof.context -> tactic) list ->
     (Proof.context -> tactic) -> typ list option -> binding ->
     binding -> binding list ->
@@ -434,22 +435,27 @@
        axioms = axioms, defs = defs, facts = facts,
        nwits = length wits, wits = wits, rel = rel};
 
-fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
+fun map_bnf f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16
+  (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
   dead = dead, deads = deads, map = map, sets = sets, bd = bd,
   axioms = axioms, defs = defs, facts = facts,
   nwits = nwits, wits = wits, rel = rel}) =
-  BNF {name = Morphism.binding phi name, T = Morphism.typ phi T,
-    live = live, lives = List.map (Morphism.typ phi) lives,
-    lives' = List.map (Morphism.typ phi) lives',
-    dead = dead, deads = List.map (Morphism.typ phi) deads,
-    map = Morphism.term phi map, sets = List.map (Morphism.term phi) sets,
-    bd = Morphism.term phi bd,
-    axioms = morph_axioms phi axioms,
-    defs = morph_defs phi defs,
-    facts = morph_facts phi facts,
-    nwits = nwits,
-    wits = List.map (morph_witness phi) wits,
-    rel = Morphism.term phi rel};
+  BNF {name = f1 name, T = f2 T,
+       live = f3 live, lives = f4 lives, lives' = f5 lives', dead = f6 dead, deads = f7 deads,
+       map = f8 map, sets = f9 sets, bd = f10 bd,
+       axioms = f11 axioms, defs = f12 defs, facts = f13 facts,
+       nwits = f14 nwits, wits = f15 wits, rel = f16 rel};
+
+fun morph_bnf phi =
+  let
+    val Tphi = Morphism.typ phi;
+    val tphi = Morphism.term phi;
+  in
+    map_bnf (Morphism.binding phi) Tphi I (map Tphi) (map Tphi) I (map Tphi) tphi (map tphi) tphi
+      (morph_axioms phi) (morph_defs phi) (morph_facts phi) I (map (morph_witness phi)) tphi
+  end;
+
+fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I;
 
 structure Data = Generic_Data
 (
@@ -660,7 +666,7 @@
 
 (* Define new BNFs *)
 
-fun define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
+fun define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
   ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy =
   let
     val live = length set_rhss;
@@ -683,8 +689,9 @@
           ((rhs, Drule.reflexive_thm), lthy)
         else
           let val b = b () in
-            apfst (apsnd snd) (Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs))
-              lthy)
+            apfst (apsnd snd)
+              ((if internal then Local_Theory.define_internal else Local_Theory.define)
+                ((b, NoSyn), ((Thm.def_binding b, []), rhs)) lthy)
           end
       end;
 
@@ -830,8 +837,8 @@
      (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy)
   end;
 
-fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs
-  ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
+fun prepare_def const_policy mk_fact_policy internal qualify prep_typ prep_term Ds_opt map_b rel_b
+  set_bs ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
   no_defs_lthy =
   let
     val fact_policy = mk_fact_policy no_defs_lthy;
@@ -861,7 +868,7 @@
      (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
      (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
      (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) =
-       define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
+       define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
          ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy;
 
     val dead = length deads;
@@ -1304,7 +1311,7 @@
   (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))) lthy);
 
-fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
+fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
   (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
   let
     fun mk_wits_tac ctxt set_maps =
@@ -1324,7 +1331,7 @@
       goals (map (fn tac => fn {context = ctxt, prems = _} =>
         unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
     |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
-  end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs;
+  end) oo prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs;
 
 val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
   let
@@ -1343,8 +1350,8 @@
     Proof.unfolding ([[(defs, [])]])
       (Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms)
         (map (single o rpair []) goals @ nontriv_wit_goals) lthy)
-  end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_typ Syntax.read_term NONE
-    Binding.empty Binding.empty [];
+  end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
+    NONE Binding.empty Binding.empty [];
 
 fun print_bnfs ctxt =
   let

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Sun Mar 09 22:45:09 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 10 13:23:16 2014 +0100
@@ -2088,7 +2088,7 @@
         val (Jbnf_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 all_witss Ts lthy;
@@ -2516,7 +2516,7 @@
         val (Jbnfs, lthy) =
           fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms =>
               fn consts => fn lthy =>
-            bnf_def Do_Inline (user_policy Note_Some) I tacs (wit_tac Jwit_thms) (SOME deads)
+            bnf_def Do_Inline (user_policy Note_Some) false I tacs (wit_tac Jwit_thms) (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 Jwit_thmss

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Mar 09 22:45:09 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 10 13:23:16 2014 +0100
@@ -1483,7 +1483,7 @@
         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;
@@ -1769,7 +1769,7 @@
 
         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