# HG changeset patch
# User blanchet
# Date 1346312866 -7200
# Node ID 8fd8d8be11858d99e278bb6212dba4a05d265e6c
# Parent  f379cf5d71bdcbc002890e48a7b584f8037cbdff
tuning

diff -r f379cf5d71bd -r 8fd8d8be1185 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -556,10 +556,10 @@
           else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_witN i) b) (1 upto nwits);
       in map2 pair bs wit_rhss end;
 
-    fun maybe_define needed_for_fp (b, rhs) lthy =
+    fun maybe_define needed_for_extra_facts (b, rhs) lthy =
       let
         val inline =
-          (not needed_for_fp orelse fact_policy = Derive_Some_Facts) andalso
+          (not needed_for_extra_facts orelse fact_policy = Derive_Some_Facts) andalso
           (case const_policy of
             Dont_Inline => false
           | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs