# HG changeset patch
# User blanchet
# Date 1284380993 -7200
# Node ID 1c2ed6dc44427bac2cc31202a6289ce61dae4395
# Parent  ffa577c0bbfa9d975341cb87403e2aeb7bb207d3
tuning

diff -r ffa577c0bbfa -r 1c2ed6dc4442 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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)