pass relevant options from "sledgehammer" to "sledgehammer minimize";
one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 21 14:46:29 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 21 16:21:19 2010 +0200
@@ -9,6 +9,7 @@
 signature ATP_MANAGER =
 sig
   type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+  type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
   type params =
     {debug: bool,
      verbose: bool,
@@ -41,7 +42,8 @@
      proof: string,
      internal_thm_names: string Vector.vector,
      filtered_clauses: (thm * (string * int)) list}
-  type prover = params -> Time.time -> problem -> prover_result
+  type prover =
+    params -> minimize_command -> Time.time -> problem -> prover_result
 
   val atps: string Unsynchronized.ref
   val timeout: int Unsynchronized.ref
@@ -52,7 +54,9 @@
   val add_prover: string * prover -> theory -> theory
   val get_prover: theory -> string -> prover option
   val available_atps: theory -> unit
-  val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
+  val sledgehammer:
+    params -> int -> relevance_override -> (string -> minimize_command)
+    -> Proof.state -> unit
 end;
 
 structure ATP_Manager : ATP_MANAGER =
@@ -62,7 +66,7 @@
 open Sledgehammer_Fact_Filter
 open Sledgehammer_Proof_Reconstruct
 
-(** parameters, problems, results, and provers **)
+(** problems, results, provers, etc. **)
 
 type params =
   {debug: bool,
@@ -99,7 +103,8 @@
    internal_thm_names: string Vector.vector,
    filtered_clauses: (thm * (string * int)) list};
 
-type prover = params -> Time.time -> problem -> prover_result;
+type prover =
+  params -> minimize_command -> Time.time -> problem -> prover_result
 
 
 (** preferences **)
@@ -323,12 +328,12 @@
   val empty = Symtab.empty;
   val extend = I;
   fun merge data : T = Symtab.merge (eq_snd op =) data
-    handle Symtab.DUP dup => err_dup_prover dup;
+    handle Symtab.DUP name => err_dup_prover name;
 );
 
 fun add_prover (name, prover) thy =
   Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
-    handle Symtab.DUP dup => err_dup_prover dup;
+    handle Symtab.DUP name => err_dup_prover name;
 
 fun get_prover thy name =
   Option.map #1 (Symtab.lookup (Provers.get thy) name);
@@ -341,7 +346,7 @@
 (* start prover thread *)
 
 fun start_prover (params as {timeout, ...}) birth_time death_time i
-                 relevance_override proof_state name =
+                 relevance_override minimize_command proof_state name =
   (case get_prover (Proof.theory_of proof_state) name of
     NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
   | SOME prover =>
@@ -359,7 +364,8 @@
               {subgoal = i, goal = (ctxt, (facts, goal)),
                relevance_override = relevance_override, axiom_clauses = NONE,
                filtered_clauses = NONE}
-            val message = #message (prover params timeout problem)
+            val message =
+              #message (prover params (minimize_command name) timeout problem)
               handle Sledgehammer_HOL_Clause.TRIVIAL =>
                   metis_line i n []
                 | ERROR msg => "Error: " ^ msg ^ ".\n";
@@ -371,14 +377,15 @@
 (* Sledgehammer the given subgoal *)
 
 fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
-                 proof_state =
+                 minimize_command proof_state =
   let
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
     val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
     val _ = priority "Sledgehammering..."
     val _ = List.app (start_prover params birth_time death_time i
-                                   relevance_override proof_state) atps
+                                   relevance_override minimize_command
+                                   proof_state) atps
   in () end
 
 end;

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 21 14:46:29 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 21 16:21:19 2010 +0200
@@ -78,7 +78,7 @@
       axiom_clauses = SOME axclauses,
       filtered_clauses = SOME (the_default axclauses filtered_clauses)}
   in
-    `outcome_of_result (prover params timeout problem)
+    `outcome_of_result (prover params (K "") timeout problem)
     |>> tap (priority o string_of_outcome)
   end
 
@@ -122,8 +122,8 @@
             ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
         in
           (SOME min_thms,
-           proof_text isar_proof true modulus sorts atp_name proof
-                      internal_thm_names ctxt goal i |> fst)
+           proof_text isar_proof modulus sorts ctxt (K "") proof
+                      internal_thm_names goal i |> fst)
         end
     | (Timeout, _) =>
         (NONE, "Timeout: You can increase the time limit using the \"timeout\" \

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 14:46:29 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 16:21:19 2010 +0200
@@ -73,6 +73,7 @@
 
 fun generic_prover overlord get_facts prepare write_file cmd args known_failures
         proof_text name ({debug, full_types, explicit_apply, ...} : params)
+        minimize_command
         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
          : problem) =
   let
@@ -105,7 +106,7 @@
       in
         if destdir' = "" then File.tmp_path probfile
         else if File.exists (Path.explode destdir')
-        then Path.append  (Path.explode destdir') probfile
+        then Path.append (Path.explode destdir') probfile
         else error ("No such directory: " ^ destdir' ^ ".")
       end;
 
@@ -154,7 +155,7 @@
     val success = rc = 0 andalso failure = "";
     val (message, relevant_thm_names) =
       if success then
-        proof_text name proof internal_thm_names ctxt th subgoal
+        proof_text ctxt minimize_command proof internal_thm_names th subgoal
       else if failure <> "" then
         (failure, [])
       else
@@ -176,7 +177,7 @@
         (params as {debug, overlord, respect_no_atp, relevance_threshold,
                     convergence, theory_relevant, higher_order, follow_defs,
                     isar_proof, modulus, sorts, ...})
-        timeout =
+        minimize_command timeout =
   generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
@@ -184,8 +185,8 @@
       (prepare_clauses higher_order false)
       (write_tptp_file (debug andalso overlord andalso not isar_proof)) command
       (arguments timeout) known_failures
-      (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts)
-      name params
+      (proof_text (supports_isar_proofs andalso isar_proof) modulus sorts)
+      name params minimize_command
 
 fun tptp_prover name p = (name, generic_tptp_prover (name, p));
 
@@ -240,14 +241,14 @@
                  prefers_theory_relevant, ...} : prover_config))
         (params as {overlord, respect_no_atp, relevance_threshold, convergence,
                     theory_relevant, higher_order, follow_defs, ...})
-        timeout =
+        minimize_command timeout =
   generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses higher_order true) write_dfg_file command
-      (arguments timeout) known_failures (metis_proof_text false false)
-      name params
+      (arguments timeout) known_failures (K metis_proof_text)
+      name params minimize_command
 
 fun dfg_prover name p = (name, generic_dfg_prover (name, p))
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 21 14:46:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 21 16:21:19 2010 +0200
@@ -68,6 +68,10 @@
    ("metis_proof", "isar_proof"),
    ("no_sorts", "sorts")]
 
+val params_for_minimize =
+  ["full_types", "explicit_apply", "higher_order", "isar_proof", "modulus",
+   "sorts", "minimize_timeout"]
+
 val property_dependent_params = ["atps", "full_types", "timeout"]
 
 fun is_known_raw_param s =
@@ -219,18 +223,33 @@
 val refresh_tptpN = "refresh_tptp"
 val helpN = "help"
 
-
 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) =
+  key ^ (case space_implode " " values of
+           "" => ""
+         | value => " = " ^ value)
+
+fun minimize_command override_params i atp_name facts =
+  "sledgehammer minimize [atp = " ^ atp_name ^
+  (override_params |> filter is_raw_param_relevant_for_minimize
+                   |> implode o map (prefix ", " o string_for_raw_param)) ^
+  "] (" ^ space_implode " " facts ^ ")" ^
+  (if i = 1 then "" else " " ^ string_of_int i)
+
 fun hammer_away override_params subcommand opt_i relevance_override state =
   let
     val thy = Proof.theory_of state
     val _ = List.app check_raw_param override_params
   in
     if subcommand = runN then
-      sledgehammer (get_params thy override_params) (the_default 1 opt_i)
-                   relevance_override state
+      let val i = the_default 1 opt_i in
+        sledgehammer (get_params thy override_params) i relevance_override
+                     (minimize_command override_params i) state
+      end
     else if subcommand = minimizeN then
       minimize (map (apfst minimizize_raw_param_name) override_params) []
                (the_default 1 opt_i) (#add relevance_override) state

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 21 14:46:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 21 16:21:19 2010 +0200
@@ -6,6 +6,8 @@
 
 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
 sig
+  type minimize_command = string list -> string
+
   val chained_hint: string
   val invert_const: string -> string
   val invert_type_const: string -> string
@@ -15,14 +17,14 @@
   val is_proof_well_formed: string -> bool
   val metis_line: int -> int -> string list -> string
   val metis_proof_text:
-    bool -> bool -> string -> string -> string vector -> Proof.context -> thm
-    -> int -> string * string list
+    minimize_command -> string -> string vector -> thm -> int
+    -> string * string list
   val isar_proof_text:
-    bool -> int -> bool -> string -> string -> string vector -> Proof.context
+    int -> bool -> Proof.context -> minimize_command -> string -> string vector
     -> thm -> int -> string * string list
   val proof_text:
-    bool -> bool -> int -> bool -> string -> string -> string vector
-    -> Proof.context -> thm -> int -> string * string list
+    bool -> int -> bool -> Proof.context -> minimize_command -> string
+    -> string vector -> thm -> int -> string * string list
 end;
 
 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -31,6 +33,8 @@
 open Sledgehammer_FOL_Clause
 open Sledgehammer_Fact_Preprocessor
 
+type minimize_command = string list -> string
+
 val trace_proof_path = Path.basic "atp_trace";
 
 fun trace_proof_msg f =
@@ -528,16 +532,15 @@
 fun metis_line i n xs =
   "Try this command: " ^
   Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
-fun minimize_line _ _ [] = ""
-  | minimize_line isar_proof atp_name xs =
+fun minimize_line _ [] = ""
+  | minimize_line minimize_command facts =
+    case minimize_command facts of
+      "" => ""
+    | command =>
       "To minimize the number of lemmas, try this command: " ^
-      Markup.markup Markup.sendback
-                    ("sledgehammer minimize [atp = " ^ atp_name ^
-                     (if isar_proof then ", isar_proof" else "") ^ "] (" ^
-                     space_implode " " xs ^ ")") ^ ".\n"
+      Markup.markup Markup.sendback command ^ ".\n"
 
-fun metis_proof_text isar_proof minimal atp_name proof thm_names
-                     (_ : Proof.context) goal i =
+fun metis_proof_text minimize_command proof thm_names goal i =
   let
     val lemmas =
       proof |> get_proof_extract
@@ -549,12 +552,10 @@
     val n = Logic.count_prems (prop_of goal)
     val xs = kill_chained lemmas
   in
-    (metis_line i n xs ^
-     (if minimal then "" else minimize_line isar_proof atp_name xs),
-     kill_chained lemmas)
+    (metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas)
   end
 
-fun isar_proof_text minimal modulus sorts atp_name proof thm_names ctxt goal i =
+fun isar_proof_text modulus sorts ctxt minimize_command proof thm_names goal i =
   let
     (* We could use "split_lines", but it can return blank lines. *)
     val lines = String.tokens (equal #"\n");
@@ -563,7 +564,7 @@
     val extract = get_proof_extract proof
     val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
     val (one_line_proof, lemma_names) =
-      metis_proof_text true minimal atp_name proof thm_names ctxt goal i
+      metis_proof_text minimize_command proof thm_names goal i
     val tokens = String.tokens (fn c => c = #" ") one_line_proof
     val isar_proof =
       if member (op =) tokens chained_hint then ""
@@ -575,8 +576,7 @@
      lemma_names)
   end
 
-fun proof_text isar_proof minimal modulus sorts =
-  if isar_proof then isar_proof_text minimal modulus sorts
-  else metis_proof_text isar_proof minimal
+fun proof_text isar_proof modulus sorts ctxt =
+  if isar_proof then isar_proof_text modulus sorts ctxt else metis_proof_text
 
 end;