1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -172,7 +172,8 @@
     1.4                     facts =
     1.5    let
     1.6      val ctxt = Proof.context_of state
     1.7 -    val prover = get_prover ctxt Minimize prover_name
     1.8 +    val prover =
     1.9 +      get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
    1.10      val _ = print silent (fn () => "Sledgehammer minimizer: " ^
    1.11                                     quote prover_name ^ ".")
    1.12      fun test timeout = test_facts params silent prover timeout i n state

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4    type minimize_command = ATP_Reconstruct.minimize_command
     2.5    type relevance_fudge = Sledgehammer_Filter.relevance_fudge
     2.6  
     2.7 -  datatype mode = Auto_Try | Try | Normal | Minimize
     2.8 +  datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
     2.9  
    2.10    type params =
    2.11      {debug: bool,
    2.12 @@ -126,7 +126,7 @@
    2.13  
    2.14  (** The Sledgehammer **)
    2.15  
    2.16 -datatype mode = Auto_Try | Try | Normal | Minimize
    2.17 +datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
    2.18  
    2.19  (* Identifier that distinguishes Sledgehammer from other tools that could use
    2.20     "Async_Manager". *)
    2.21 @@ -566,6 +566,7 @@
    2.22  fun suffix_for_mode Auto_Try = "_auto_try"
    2.23    | suffix_for_mode Try = "_try"
    2.24    | suffix_for_mode Normal = ""
    2.25 +  | suffix_for_mode Auto_Minimize = "_auto_min"
    2.26    | suffix_for_mode Minimize = "_min"
    2.27  
    2.28  (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on