src/HOL/ex/sledgehammer_tactics.ML
changeset 44625 4a1132815a70
parent 44586 eeba1eedf32d
child 44651 5d6a11e166cf
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 31 11:23:16 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 31 11:52:03 2011 +0200
     1.3 @@ -37,13 +37,11 @@
     1.4      val relevance_fudge =
     1.5        Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
     1.6      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     1.7 -    val is_ho_atp =
     1.8 -      exists (Sledgehammer_Provers.is_ho_atp ctxt)
     1.9 -        provers(*FIXME: duplicated from sledgehammer_run.ML*)
    1.10 +    val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
    1.11      val facts =
    1.12 -      Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
    1.13 +      Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
    1.14                                             chained_ths hyp_ts concl_t
    1.15 -      |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
    1.16 +      |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    1.17               (the_default default_max_relevant max_relevant) is_built_in_const
    1.18               relevance_fudge relevance_override chained_ths hyp_ts concl_t
    1.19      val problem =