--- a/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -2859,11 +2859,9 @@
val wit_tac = mk_wit_tac n dtor_ctor_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
- val policy = user_policy Derive_All_Facts_Note_Most;
-
val (Jbnfs, lthy) =
fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy =>
- bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads)
+ bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads)
(((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs fs_maps setss_by_bnf Ts all_witss lthy;