# HG changeset patch
# User blanchet
# Date 1307571388 -7200
# Node ID 03e6da81aee677232938d722a2127bf3aee8e8ba
# Parent  8b59c1d87fd684bbe3174eff23bcb5803b6bbd89
tuning

diff -r 8b59c1d87fd6 -r 03e6da81aee6 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -109,7 +109,7 @@
 
 fun binary_minimize test xs =
   let
-    fun p xs = #outcome (test xs : prover_result) = NONE
+    fun pred xs = #outcome (test xs : prover_result) = NONE
     fun split [] p = p
       | split [h] (l, r) = (h :: l, r)
       | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
@@ -124,9 +124,9 @@
 *)
           val (l0, r0) = split xs ([], [])
         in
-          if p (sup @ l0) then
+          if pred (sup @ l0) then
             min (depth + 1) sup l0
-          else if p (sup @ r0) then
+          else if pred (sup @ r0) then
             min (depth + 1) sup r0
           else
             let
@@ -139,7 +139,7 @@
 *)
     val xs =
       case min 0 [] xs of
-        [x] => if p [] then [] else [x]
+        [x] => if pred [] then [] else [x]
       | xs => xs
   in (xs, test xs) end
 
diff -r 8b59c1d87fd6 -r 03e6da81aee6 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -18,8 +18,8 @@
   val noneN : string
   val timeoutN : string
   val unknownN : string
-  val auto_minimize_min_facts : int Config.T
-  val auto_minimize_max_time : real Config.T
+  val auto_min_min_facts : int Config.T
+  val auto_min_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,12 +66,11 @@
     else
       "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
 
-val auto_minimize_min_facts =
-  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
+val auto_min_min_facts =
+  Attrib.setup_config_int @{binding sledgehammer_auto_min_min_facts}
       (fn generic => Config.get_generic generic binary_min_facts)
-val auto_minimize_max_time =
-  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
-      (K 5.0)
+val auto_min_max_time =
+  Attrib.setup_config_real @{binding sledgehammer_auto_min_max_time} (K 0.0) (*###*)
 
 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
@@ -84,13 +83,13 @@
       val num_facts = length used_facts
       val ((minimize, minimize_name), preplay) =
         if mode = Normal then
-          if num_facts >= Config.get ctxt auto_minimize_min_facts then
+          if num_facts >= Config.get ctxt auto_min_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_minimize_max_time
+                <= Config.get ctxt auto_min_max_time
               val prover_fast_enough =
                 run_time_in_msecs |> Option.map can_min_fast_enough
                                   |> the_default false