# HG changeset patch
# User bulwahn
# Date 1297434679 -3600
# Node ID e4dbd12a3d8373fc18923802a2135cb57c04da31
# Parent  404d94506599d9ef405a20b7626518b6f6f86a29# Parent  949eaf045e009b11d36e4618aa942e1a58350676
merged

diff -r 404d94506599 -r e4dbd12a3d83 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Feb 11 11:47:44 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Feb 11 15:31:19 2011 +0100
@@ -10,6 +10,7 @@
 val keepK = "keep"
 val full_typesK = "full_types"
 val type_sysK = "type_sys"
+val max_relevantK = "max_relevant"
 val minimizeK = "minimize"
 val minimize_timeoutK = "minimize_timeout"
 val metis_ftK = "metis_ft"
@@ -347,7 +348,7 @@
   SH_FAIL of int * int |
   SH_ERROR
 
-fun run_sh prover_name prover type_sys hard_timeout timeout dir st =
+fun run_sh prover_name prover type_sys max_relevant hard_timeout timeout dir st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
@@ -365,6 +366,7 @@
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
            ("type_sys", type_sys),
+           ("max_relevant", max_relevant),
            ("timeout", string_of_int timeout)]
     val default_max_relevant =
       Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name
@@ -428,13 +430,14 @@
     val _ = if trivial then () else change_data id inc_sh_nontriv_calls
     val (prover_name, prover) = get_prover (Proof.context_of st) args
     val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
+    val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
     val dir = AList.lookup (op =) args keepK
     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
     (* always use a hard timeout, but give some slack so that the automatic
        minimizer has a chance to do its magic *)
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
-      run_sh prover_name prover type_sys hard_timeout timeout dir st
+      run_sh prover_name prover type_sys max_relevant hard_timeout timeout dir st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>