src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
changeset 43351 b19d95b4d736
parent 43088 0a97f3295642
child 43710 7270ae921cf2
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Jun 09 23:30:18 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jun 10 12:01:15 2011 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4      (case Prooftab.lookup (!proof_table) (line_num, col_num) of
     1.5         SOME proofs =>
     1.6         let
     1.7 -         val {context = ctxt, facts, goal} = Proof.goal pre
     1.8 +         val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
     1.9           val prover = AList.lookup (op =) args "prover"
    1.10                        |> the_default default_prover
    1.11           val {relevance_thresholds, max_relevant, slicing, ...} =
    1.12 @@ -130,10 +130,13 @@
    1.13           val subgoal = 1
    1.14           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
    1.15           val facts =
    1.16 -           Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    1.17 -               (the_default default_max_relevant max_relevant)
    1.18 -               is_appropriate_prop is_built_in_const relevance_fudge
    1.19 -               relevance_override facts hyp_ts concl_t
    1.20 +          Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
    1.21 +                                               chained_ths hyp_ts concl_t
    1.22 +          |> filter (is_appropriate_prop o prop_of o snd)
    1.23 +          |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    1.24 +                 (the_default default_max_relevant max_relevant)
    1.25 +                 is_built_in_const relevance_fudge relevance_override
    1.26 +                 chained_ths hyp_ts concl_t
    1.27             |> map (fst o fst)
    1.28           val (found_facts, lost_facts) =
    1.29             flat proofs |> sort_distinct string_ord