# HG changeset patch
# User blanchet
# Date 1315817377 -7200
# Node ID a41eacd1ae8db7ff24c9ac433bd6243d425fbc67
# Parent  0ff207302573d3a4b15c5aa482342328bbcce0b9
consistent option naming

diff -r 0ff207302573 -r a41eacd1ae8d src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- 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