changed policy when to define constants
authortraytel
Tue Mar 18 14:32:23 2014 +0100 (2014-03-18)
changeset 56192d666cb0e4cf9
parent 56191 159b0c88b4a4
child 56193 c726ecfb22b6
changed policy when to define constants
src/HOL/Tools/BNF/bnf_lfp.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 18 11:47:59 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 18 14:32:23 2014 +0100
     1.3 @@ -1483,7 +1483,7 @@
     1.4          val (Ibnf_consts, lthy) =
     1.5            fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
     1.6                fn T => fn lthy =>
     1.7 -            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads)
     1.8 +            define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
     1.9                map_b rel_b set_bs
    1.10                ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
    1.11            bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;