# HG changeset patch
# User blanchet
# Date 1271257816 -7200
# Node ID c31602d268bef25ccc4fa82bba773a2aab61af59
# Parent  08b2a7ecb6c3349ff8ee504fcb55dad86973be41
make Sledgehammer's "timeout" option work for "minimize"

diff -r 08b2a7ecb6c3 -r c31602d268be src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 16:50:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 17:10:16 2010 +0200
@@ -156,7 +156,7 @@
 fun get_params thy = extract_params thy (default_raw_params thy)
 fun default_params thy = get_params thy o map (apsnd single)
 
-fun atp_minimize_command override_params old_style_args i fact_refs state =
+fun minimize override_params old_style_args i fact_refs state =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -205,6 +205,9 @@
 val delN = "del"
 val onlyN = "only"
 
+fun minimizize_raw_param_name "timeout" = "minimize_timeout"
+  | minimizize_raw_param_name name = name
+
 fun hammer_away override_params subcommand opt_i relevance_override state =
   let
     val thy = Proof.theory_of state
@@ -214,8 +217,8 @@
       sledgehammer (get_params thy override_params) (the_default 1 opt_i)
                    relevance_override state
     else if subcommand = minimizeN then
-      atp_minimize_command override_params [] (the_default 1 opt_i)
-                           (#add relevance_override) state
+      minimize (map (apfst minimizize_raw_param_name) 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
@@ -300,8 +303,7 @@
     "minimize theorem list with external prover" K.diag
     (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
       Toplevel.no_timing o Toplevel.unknown_proof o
-        Toplevel.keep (atp_minimize_command [] args 1 fact_refs
-                       o Toplevel.proof_of)))
+        Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of)))
 
 val _ =
   OuterSyntax.improper_command "sledgehammer"