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 @@ -113,11 +113,10 @@
     1.4           val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
     1.5           val prover = AList.lookup (op =) args "prover"
     1.6                        |> the_default default_prover
     1.7 -         val params as {max_relevant, slice, ...} =
     1.8 +         val params as {max_facts, slice, ...} =
     1.9             Sledgehammer_Isar.default_params ctxt args
    1.10 -         val default_max_relevant =
    1.11 -           Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
    1.12 -                                                                prover
    1.13 +         val default_max_facts =
    1.14 +           Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover
    1.15           val is_appropriate_prop =
    1.16             Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt
    1.17                 default_prover
    1.18 @@ -132,7 +131,7 @@
    1.19                 Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
    1.20             |> filter (is_appropriate_prop o prop_of o snd)
    1.21             |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    1.22 -                  default_prover (the_default default_max_relevant max_relevant)
    1.23 +                  default_prover (the_default default_max_facts max_facts)
    1.24                    (SOME relevance_fudge) hyp_ts concl_t
    1.25              |> map ((fn name => name ()) o fst o fst)
    1.26           val (found_facts, lost_facts) =