src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 41269 abe867c29e55
parent 41267 958fee9ec275
child 41316 558afd8b94d6
--- 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