# HG changeset patch
# User blanchet
# Date 1304597938 -7200
# Node ID d7c127478ee14e4c70620dde4e6365174d81e49e
# Parent  500e4a88675e3ae2fd62780083e235d276ee69ef
tuning

diff -r 500e4a88675e -r d7c127478ee1 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 05 14:04:40 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 05 14:18:58 2011 +0200
@@ -528,7 +528,7 @@
   else
     tab
 
-fun add_arities is_built_in_const th =
+fun consider_arities is_built_in_const th =
   let
     fun aux _ _ NONE = NONE
       | aux t args (SOME tab) =
@@ -543,8 +543,9 @@
         | _ => SOME tab
   in aux (prop_of th) [] end
 
-fun needs_ext is_built_in_const facts =
-  fold (add_arities is_built_in_const o snd) facts (SOME Symtab.empty)
+(* FIXME: This is currently only useful for polymorphic type systems. *)
+fun could_benefit_from_ext is_built_in_const facts =
+  fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
   |> is_none
 
 fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
@@ -640,7 +641,7 @@
           |> iter 0 max_relevant threshold0 goal_const_tab []
           |> not (null add_ths) ? add_facts add_ths
           |> (fn accepts =>
-                 accepts |> needs_ext is_built_in_const accepts
+                 accepts |> could_benefit_from_ext is_built_in_const accepts
                             ? add_facts @{thms ext})
           |> tap (fn accepts => trace_msg ctxt (fn () =>
                       "Total relevant: " ^ string_of_int (length accepts)))