1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 05 14:04:40 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 05 14:18:58 2011 +0200
     1.3 @@ -528,7 +528,7 @@
     1.4    else
     1.5      tab
     1.6  
     1.7 -fun add_arities is_built_in_const th =
     1.8 +fun consider_arities is_built_in_const th =
     1.9    let
    1.10      fun aux _ _ NONE = NONE
    1.11        | aux t args (SOME tab) =
    1.12 @@ -543,8 +543,9 @@
    1.13          | _ => SOME tab
    1.14    in aux (prop_of th) [] end
    1.15  
    1.16 -fun needs_ext is_built_in_const facts =
    1.17 -  fold (add_arities is_built_in_const o snd) facts (SOME Symtab.empty)
    1.18 +(* FIXME: This is currently only useful for polymorphic type systems. *)
    1.19 +fun could_benefit_from_ext is_built_in_const facts =
    1.20 +  fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
    1.21    |> is_none
    1.22  
    1.23  fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
    1.24 @@ -640,7 +641,7 @@
    1.25            |> iter 0 max_relevant threshold0 goal_const_tab []
    1.26            |> not (null add_ths) ? add_facts add_ths
    1.27            |> (fn accepts =>
    1.28 -                 accepts |> needs_ext is_built_in_const accepts
    1.29 +                 accepts |> could_benefit_from_ext is_built_in_const accepts
    1.30                              ? add_facts @{thms ext})
    1.31            |> tap (fn accepts => trace_msg ctxt (fn () =>
    1.32                        "Total relevant: " ^ string_of_int (length accepts)))