1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    type minimize_command = ATP_Reconstruct.minimize_command
     1.5    type relevance_fudge = Sledgehammer_Filter.relevance_fudge
     1.6  
     1.7 -  datatype mode = Auto_Try | Try | Normal | Minimize
     1.8 +  datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
     1.9  
    1.10    type params =
    1.11      {debug: bool,
    1.12 @@ -126,7 +126,7 @@
    1.13  
    1.14  (** The Sledgehammer **)
    1.15  
    1.16 -datatype mode = Auto_Try | Try | Normal | Minimize
    1.17 +datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
    1.18  
    1.19  (* Identifier that distinguishes Sledgehammer from other tools that could use
    1.20     "Async_Manager". *)
    1.21 @@ -566,6 +566,7 @@
    1.22  fun suffix_for_mode Auto_Try = "_auto_try"
    1.23    | suffix_for_mode Try = "_try"
    1.24    | suffix_for_mode Normal = ""
    1.25 +  | suffix_for_mode Auto_Minimize = "_auto_min"
    1.26    | suffix_for_mode Minimize = "_min"
    1.27  
    1.28  (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on