# HG changeset patch
# User blanchet
# Date 1321613232 -3600
# Node ID 7a39df11bcf6f28b0a0b28bed27a6fe99da53f35
# Parent  22d003b5b32e767bbdaca56ef238fb3b1d25a79b
be more silent when auto minimizing

diff -r 22d003b5b32e -r 7a39df11bcf6 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -172,7 +172,8 @@
                    facts =
   let
     val ctxt = Proof.context_of state
-    val prover = get_prover ctxt Minimize prover_name
+    val prover =
+      get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
     val _ = print silent (fn () => "Sledgehammer minimizer: " ^
                                    quote prover_name ^ ".")
     fun test timeout = test_facts params silent prover timeout i n state
diff -r 22d003b5b32e -r 7a39df11bcf6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -16,7 +16,7 @@
   type minimize_command = ATP_Reconstruct.minimize_command
   type relevance_fudge = Sledgehammer_Filter.relevance_fudge
 
-  datatype mode = Auto_Try | Try | Normal | Minimize
+  datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
 
   type params =
     {debug: bool,
@@ -126,7 +126,7 @@
 
 (** The Sledgehammer **)
 
-datatype mode = Auto_Try | Try | Normal | Minimize
+datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
 
 (* Identifier that distinguishes Sledgehammer from other tools that could use
    "Async_Manager". *)
@@ -566,6 +566,7 @@
 fun suffix_for_mode Auto_Try = "_auto_try"
   | suffix_for_mode Try = "_try"
   | suffix_for_mode Normal = ""
+  | suffix_for_mode Auto_Minimize = "_auto_min"
   | suffix_for_mode Minimize = "_min"
 
 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on