--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Sep 13 14:29:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Sep 13 14:29:53 2010 +0200
@@ -374,8 +374,7 @@
fun run_prover (params as {blocking, verbose, max_relevant, timeout, expect,
...})
- auto i n relevance_override minimize_command
- (problem as {state, goal, axioms, ...})
+ auto i n minimize_command (problem as {state, goal, axioms, ...})
(prover as {default_max_relevant, ...}, atp_name) =
let
val ctxt = Proof.context_of state
@@ -461,10 +460,7 @@
val problem =
{state = state, goal = goal, subgoal = i,
axioms = map (prepare_axiom ctxt) axioms}
- val run_prover =
- run_prover params auto i n relevance_override minimize_command
- problem
- val num_axioms = length axioms
+ val run_prover = run_prover params auto i n minimize_command problem
in
if auto then
fold (fn prover => fn (true, state) => (true, state)