1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 21 16:37:28 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 22 16:59:27 2012 +0200
     1.3 @@ -391,8 +391,8 @@
     1.4        | (Abs (_, T, t'), ts) =>
     1.5          ((null ts andalso not ext_arg)
     1.6           (* Since lambdas on the right-hand side of equalities are usually
     1.7 -            extensionalized later by "extensionalize_term", we don't penalize
     1.8 -            them here. *)
     1.9 +            extensionalized later by "abs_extensionalize_term", we don't
    1.10 +            penalize them here. *)
    1.11           ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
    1.12          #> fold (do_term false) (t' :: ts)
    1.13        | (_, ts) => fold (do_term false) ts