--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Sep 12 09:07:23 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Sep 12 10:49:37 2011 +0200
@@ -18,8 +18,8 @@
val noneN : string
val timeoutN : string
val unknownN : string
- val auto_min_min_facts : int Config.T
- val auto_min_max_time : real Config.T
+ val auto_minimize_min_facts : int Config.T
+ val auto_minimize_max_time : real Config.T
val get_minimizing_prover : Proof.context -> mode -> string -> prover
val run_sledgehammer :
params -> mode -> int -> relevance_override -> (string -> minimize_command)
@@ -66,11 +66,12 @@
else
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
-val auto_min_min_facts =
- Attrib.setup_config_int @{binding sledgehammer_auto_min_min_facts}
+val auto_minimize_min_facts =
+ Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
(fn generic => Config.get_generic generic binary_min_facts)
-val auto_min_max_time =
- Attrib.setup_config_real @{binding sledgehammer_auto_min_max_time} (K 5.0)
+val auto_minimize_max_time =
+ Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
+ (K 5.0)
fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
@@ -83,13 +84,13 @@
val num_facts = length used_facts
val ((minimize, minimize_name), preplay) =
if mode = Normal then
- if num_facts >= Config.get ctxt auto_min_min_facts then
+ if num_facts >= Config.get ctxt auto_minimize_min_facts then
((true, name), preplay)
else
let
fun can_min_fast_enough msecs =
0.001 * Real.fromInt ((num_facts + 2) * msecs)
- <= Config.get ctxt auto_min_max_time
+ <= Config.get ctxt auto_minimize_max_time
val prover_fast_enough =
run_time_in_msecs |> Option.map can_min_fast_enough
|> the_default false