--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 18 11:47:59 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 18 14:32:23 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) false (SOME deads)
+ define_bnf_consts Hardly_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;