--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 18:39:22 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 18:39:22 2011 +0200
@@ -317,13 +317,13 @@
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
-fun get_prover ctxt slicing args =
+fun get_prover ctxt args =
let
fun default_prover_name () =
hd (#provers (Sledgehammer_Isar.default_params ctxt []))
handle Empty => error "No ATP available."
fun get_prover name =
- (name, Sledgehammer_Run.get_minimizing_prover ctxt false slicing name)
+ (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name
@@ -429,7 +429,7 @@
val triv_str = if trivial then "[T] " else ""
val _ = change_data id inc_sh_calls
val _ = if trivial then () else change_data id inc_sh_nontriv_calls
- val (prover_name, prover) = get_prover (Proof.context_of st) true args
+ 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
@@ -473,7 +473,7 @@
let
val ctxt = Proof.context_of st
val n0 = length (these (!named_thms))
- val (prover_name, _) = get_prover ctxt false args
+ val (prover_name, _) = get_prover ctxt args
val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
val timeout =
AList.lookup (op =) args minimize_timeoutK