let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)

--- a/src/HOL/Tools/ATP/atp_proof.ML	Sat Dec 18 12:55:33 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sat Dec 18 13:34:32 2010 +0100
@@ -110,7 +110,7 @@
   | string_for_failure prover NoPerl = "Perl" ^ missing_message_tail prover
   | string_for_failure prover NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail prover
-  | string_for_failure prover NoRealZ3 =
+  | string_for_failure _ NoRealZ3 =
     "The environment variable \"Z3_REAL_SOLVER\" must be set to Z3's full path."
   | string_for_failure prover MalformedInput =
     "The " ^ prover ^ " problem is malformed. Please report this to the \

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Dec 18 12:55:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Dec 18 13:34:32 2010 +0100
@@ -12,7 +12,7 @@
 
   val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
   val minimize_facts :
-    params -> bool -> int -> int -> Proof.state
+    string -> params -> bool -> int -> int -> Proof.state
     -> ((string * locality) * thm list) list
     -> ((string * locality) * thm list) list option * string
   val run_minimize :
@@ -124,9 +124,8 @@
    part of the timeout. *)
 val fudge_msecs = 1000
 
-fun minimize_facts {provers = [], ...} _ _ _ _ _ = error "No prover is set."
-  | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) silent
-                   i n state facts =
+fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
+                   facts =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -177,7 +176,7 @@
     handle ERROR msg => (NONE, "Error: " ^ msg)
   end
 
-fun run_minimize params i refs state =
+fun run_minimize (params as {provers, ...}) i refs state =
   let
     val ctxt = Proof.context_of state
     val reserved = reserved_isar_keyword_table ()
@@ -188,9 +187,12 @@
   in
     case subgoal_count state of
       0 => Output.urgent_message "No subgoal!"
-    | n =>
-      (kill_provers ();
-       Output.urgent_message (#2 (minimize_facts params false i n state facts)))
+    | n => case provers of
+             [] => error "No prover is set."
+           | prover :: _ =>
+             (kill_provers ();
+              minimize_facts prover params false i n state facts
+              |> #2 |> Output.urgent_message)
   end
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 12:55:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 13:34:32 2010 +0100
@@ -13,6 +13,7 @@
   type params = Sledgehammer_Provers.params
   type prover = Sledgehammer_Provers.prover
 
+  val auto_minimization_threshold : int Unsynchronized.ref
   val get_minimizing_prover : Proof.context -> bool -> string -> prover
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
@@ -41,7 +42,7 @@
    else
      "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
 
-val implicit_minimization_threshold = 50
+val auto_minimization_threshold = Unsynchronized.ref 50
 
 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...})
         minimize_command
@@ -53,8 +54,8 @@
          else
            let
              val (used_facts, message) =
-               if length used_facts >= implicit_minimization_threshold then
-                 minimize_facts params (not verbose) subgoal subgoal_count
+               if length used_facts >= !auto_minimization_threshold then
+                 minimize_facts name params (not verbose) subgoal subgoal_count
                      state
                      (filter_used_facts used_facts
                           (map (apsnd single o untranslated_fact) facts))