# HG changeset patch
# User traytel
# Date 1395149543 -3600
# Node ID d666cb0e4cf97875cfd1c2c4f7f3d3dad79907a6
# Parent  159b0c88b4a4f1e6922bcc8b73a0a4696fe7fdfe
changed policy when to define constants

diff -r 159b0c88b4a4 -r d666cb0e4cf9 src/HOL/Tools/BNF/bnf_lfp.ML
--- 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;