get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 18 17:09:05 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 18 17:16:37 2010 +0200
@@ -389,7 +389,7 @@
       |> Option.map (fst o read_int o explode)
       |> the_default 5
     val params = Sledgehammer_Isar.default_params thy
-      [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")]
+      [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")]
     val minimize =
       Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st)
     val _ = log separator

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Aug 18 17:09:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Aug 18 17:16:37 2010 +0200
@@ -25,8 +25,7 @@
      defs_relevant: bool,
      isar_proof: bool,
      isar_shrink_factor: int,
-     timeout: Time.time,
-     minimize_timeout: Time.time}
+     timeout: Time.time}
   type problem =
     {subgoal: int,
      goal: Proof.context * (thm list * thm),
@@ -95,8 +94,7 @@
    defs_relevant: bool,
    isar_proof: bool,
    isar_shrink_factor: int,
-   timeout: Time.time,
-   minimize_timeout: Time.time}
+   timeout: Time.time}
 
 type problem =
   {subgoal: int,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Wed Aug 18 17:09:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Wed Aug 18 17:16:37 2010 +0200
@@ -58,8 +58,7 @@
        relevance_convergence = relevance_convergence,
        max_relevant_per_iter = NONE, theory_relevant = NONE,
        defs_relevant = defs_relevant, isar_proof = isar_proof,
-       isar_shrink_factor = isar_shrink_factor, timeout = timeout,
-       minimize_timeout = timeout}
+       isar_shrink_factor = isar_shrink_factor, timeout = timeout}
     val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     val {context = ctxt, facts, goal} = Proof.goal state
     val problem =
@@ -95,20 +94,18 @@
 (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
    preprocessing time is included in the estimate below but isn't part of the
    timeout. *)
-val fudge_msecs = 250
+val fudge_msecs = 1000
 
 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
   | minimize_theorems
         (params as {debug, atps = atp :: _, full_types, isar_proof,
-                    isar_shrink_factor, minimize_timeout, ...})
+                    isar_shrink_factor, timeout, ...})
         i n state name_thms_pairs =
   let
     val thy = Proof.theory_of state
     val prover = get_prover_fun thy atp
-    val msecs = Time.toMilliseconds minimize_timeout
-    val _ =
-      priority ("Sledgehammer minimize: ATP " ^ quote atp ^
-                " with a time limit of " ^ string_of_int msecs ^ " ms.")
+    val msecs = Time.toMilliseconds timeout
+    val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".")
     val {context = ctxt, goal, ...} = Proof.goal state
     val (_, hyp_ts, concl_t) = strip_subgoal goal i
     val explicit_apply =
@@ -119,7 +116,7 @@
       test_theorems params prover explicit_apply timeout i state
     val timer = Timer.startRealTimer ()
   in
-    (case do_test minimize_timeout name_thms_pairs of
+    (case do_test timeout name_thms_pairs of
        result as {outcome = NONE, pool, used_thm_names,
                   conjecture_shape, ...} =>
        let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 18 17:09:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 18 17:16:37 2010 +0200
@@ -73,8 +73,7 @@
    ("theory_relevant", "smart"),
    ("defs_relevant", "false"),
    ("isar_proof", "false"),
-   ("isar_shrink_factor", "1"),
-   ("minimize_timeout", "5 s")]
+   ("isar_shrink_factor", "1")]
 
 val alias_params =
   [("atp", "atps")]
@@ -90,7 +89,7 @@
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "full_types", "isar_proof",
-   "isar_shrink_factor", "minimize_timeout"]
+   "isar_shrink_factor", "timeout"]
 
 val property_dependent_params = ["atps", "full_types", "timeout"]
 
@@ -179,7 +178,6 @@
     val isar_proof = lookup_bool "isar_proof"
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     val timeout = lookup_time "timeout"
-    val minimize_timeout = lookup_time "minimize_timeout"
   in
     {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
      full_types = full_types, explicit_apply = explicit_apply,
@@ -188,7 +186,7 @@
      max_relevant_per_iter = max_relevant_per_iter,
      theory_relevant = theory_relevant, defs_relevant = defs_relevant,
      isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
-     timeout = timeout, minimize_timeout = minimize_timeout}
+     timeout = timeout}
   end
 
 fun get_params thy = extract_params (default_raw_params thy)
@@ -207,9 +205,6 @@
 val kill_atpsN = "kill_atps"
 val refresh_tptpN = "refresh_tptp"
 
-fun minimizize_raw_param_name "timeout" = "minimize_timeout"
-  | minimizize_raw_param_name name = name
-
 val is_raw_param_relevant_for_minimize =
   member (op =) params_for_minimize o fst o unalias_raw_param
 fun string_for_raw_param (key, values) =
@@ -233,9 +228,8 @@
                          (minimize_command override_params i) state
       end
     else if subcommand = minimizeN then
-      run_minimize (get_params thy (map (apfst minimizize_raw_param_name)
-                               override_params))
-                   (the_default 1 opt_i) (#add relevance_override) state
+      run_minimize (get_params thy override_params) (the_default 1 opt_i)
+                   (#add relevance_override) state
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = available_atpsN then