--- 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