--- 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