1.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 11 21:43:19 2012 +0200
     1.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 11 21:43:19 2012 +0200
     1.3 @@ -39,8 +39,8 @@
     1.4      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     1.5      val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
     1.6      val facts =
     1.7 -      Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
     1.8 -                                           chained_ths hyp_ts concl_t
     1.9 +      Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
    1.10 +                                         chained_ths hyp_ts concl_t
    1.11        |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    1.12               (the_default default_max_relevant max_relevant) is_built_in_const
    1.13               relevance_fudge relevance_override chained_ths hyp_ts concl_t