diff -r a96b0b62f588 -r a393d6d8e198 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- 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))