# HG changeset patch
# User blanchet
# Date 1288164160 -7200
# Node ID 80961c72c7275d57cb432a38df0433c0263ff108
# Parent  5da3e8ede850817f7fc5a36f99a56edcca360879
generalize to handle any prover (not just E)

diff -r 5da3e8ede850 -r 80961c72c727 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Oct 26 21:51:04 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Oct 27 09:22:40 2010 +0200
@@ -95,8 +95,7 @@
   else
     ()
 
-val default_max_relevant = 300
-val prover_name = ATP_Systems.eN (* arbitrary ATP *)
+val default_prover = ATP_Systems.eN (* arbitrary ATP *)
 
 fun with_index (i, s) = s ^ "@" ^ string_of_int i
 
@@ -107,11 +106,16 @@
        SOME proofs =>
        let
          val {context = ctxt, facts, goal} = Proof.goal pre
+         val thy = ProofContext.theory_of ctxt
+         val prover = AList.lookup (op =) args "prover"
+                      |> the_default default_prover
+         val default_max_relevant =
+           Sledgehammer.default_max_relevant_for_prover thy prover
          val irrelevant_consts =
-           Sledgehammer.irrelevant_consts_for_prover prover_name
+           Sledgehammer.irrelevant_consts_for_prover prover
          val relevance_fudge =
            extract_relevance_fudge args
-               (Sledgehammer.relevance_fudge_for_prover prover_name)
+               (Sledgehammer.relevance_fudge_for_prover prover)
          val relevance_override = {add = [], del = [], only = false}
          val {relevance_thresholds, full_types, max_relevant, ...} =
            Sledgehammer_Isar.default_params ctxt args