1.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 18 09:15:53 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 18 11:06:25 2012 +0200
     1.3 @@ -1700,9 +1700,11 @@
     1.4  
     1.5          fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
     1.6  
     1.7 +        val policy = user_policy Derive_All_Facts_Note_Most;
     1.8 +
     1.9          val (Ibnfs, lthy) =
    1.10            fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => fn lthy =>
    1.11 -            bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads)
    1.12 +            bnf_def Dont_Inline policy I tacs wit_tac (SOME deads)
    1.13                ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
    1.14              |> register_bnf (Local_Theory.full_name lthy b))
    1.15            tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;