tuning

--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Dec 18 13:48:24 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Dec 18 14:02:14 2010 +0100
@@ -204,7 +204,8 @@
 fun the_system name versions =
   case get_system name versions of
     SOME sys => sys
-  | NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.")
+  | NONE => error ("System " ^ quote name ^
+                   " is not available at SystemOnTPTP.")
 
 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 13:48:24 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 14:02:14 2010 +0100
@@ -13,7 +13,7 @@
   type params = Sledgehammer_Provers.params
   type prover = Sledgehammer_Provers.prover
 
-  val auto_minimization_threshold : int Unsynchronized.ref
+  val auto_minimize_threshold : int Unsynchronized.ref
   val get_minimizing_prover : Proof.context -> bool -> string -> prover
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
@@ -42,7 +42,7 @@
    else
      "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
 
-val auto_minimization_threshold = Unsynchronized.ref (!binary_threshold)
+val auto_minimize_threshold = Unsynchronized.ref (!binary_threshold)
 
 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...})
         minimize_command
@@ -54,7 +54,7 @@
          else
            let
              val (used_facts, message) =
-               if length used_facts >= !auto_minimization_threshold then
+               if length used_facts >= !auto_minimize_threshold then
                  minimize_facts name params (not verbose) subgoal subgoal_count
                      state
                      (filter_used_facts used_facts