1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -128,14 +128,14 @@
     1.4           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
     1.5           val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     1.6           val facts =
     1.7 -          Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
     1.8 -              Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
     1.9 -          |> filter (is_appropriate_prop o prop_of o snd)
    1.10 -          |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    1.11 -                 default_prover (the_default default_max_relevant max_relevant)
    1.12 -                 (SOME relevance_fudge) Sledgehammer_Fact.no_relevance_override
    1.13 -                 chained_ths hyp_ts concl_t
    1.14 -           |> map (fst o fst)
    1.15 +           Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
    1.16 +               Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
    1.17 +           |> filter (is_appropriate_prop o prop_of o snd)
    1.18 +           |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    1.19 +                  default_prover (the_default default_max_relevant max_relevant)
    1.20 +                  (SOME relevance_fudge) Sledgehammer_Fact.no_relevance_override
    1.21 +                  chained_ths hyp_ts concl_t
    1.22 +            |> map ((fn name => name ()) o fst o fst)
    1.23           val (found_facts, lost_facts) =
    1.24             flat proofs |> sort_distinct string_ord
    1.25             |> map (fn fact => (find_index (curry (op =) fact) facts, fact))