src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 43351 b19d95b4d736
parent 43261 a4aeb26a6362
child 43569 b342cd125533
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jun 09 23:30:18 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jun 10 12:01:15 2011 +0200
     1.3 @@ -408,10 +408,13 @@
     1.4          val _ = if is_appropriate_prop concl_t then ()
     1.5                  else raise Fail "inappropriate"
     1.6          val facts =
     1.7 -          Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
     1.8 -              (the_default default_max_relevant max_relevant)
     1.9 -              is_appropriate_prop is_built_in_const relevance_fudge
    1.10 -              relevance_override chained_ths hyp_ts concl_t
    1.11 +          Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
    1.12 +                                               chained_ths hyp_ts concl_t
    1.13 +          |> filter (is_appropriate_prop o prop_of o snd)
    1.14 +          |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    1.15 +                 (the_default default_max_relevant max_relevant)
    1.16 +                 is_built_in_const relevance_fudge relevance_override
    1.17 +                 chained_ths hyp_ts concl_t
    1.18          val problem =
    1.19            {state = st', goal = goal, subgoal = i,
    1.20             subgoal_count = Sledgehammer_Util.subgoal_count st,