--- 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