# HG changeset patch
# User blanchet
# Date 1409237907 -7200
# Node ID ee65e9cfe284234cded61a5bb99964cf19b10723
# Parent  9f77084444dfa5912d4248816971fa70c9c845e2
merged minimize and auto_minimize

diff -r 9f77084444df -r ee65e9cfe284 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Aug 28 16:58:27 2014 +0200
@@ -15,7 +15,7 @@
   type proof_method = Sledgehammer_Proof_Methods.proof_method
   type play_outcome = Sledgehammer_Proof_Methods.play_outcome
 
-  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
+  datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
 
   type params =
     {debug : bool,
@@ -93,18 +93,16 @@
 open Sledgehammer_Fact
 open Sledgehammer_Proof_Methods
 
-(* Identifier that distinguishes Sledgehammer from other tools that could use
-   "Async_Manager". *)
+(* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *)
 val SledgehammerN = "Sledgehammer"
 
-datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
+datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
 
 fun str_of_mode Auto_Try = "Auto Try"
   | str_of_mode Try = "Try"
   | str_of_mode Normal = "Normal"
+  | str_of_mode Minimize = "Minimize"
   | str_of_mode MaSh = "MaSh"
-  | str_of_mode Auto_Minimize = "Auto_Minimize"
-  | str_of_mode Minimize = "Minimize"
 
 val is_atp = member (op =) o supported_atps
 
diff -r 9f77084444df -r ee65e9cfe284 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Aug 28 16:58:27 2014 +0200
@@ -120,7 +120,6 @@
   | suffix_of_mode Try = "_try"
   | suffix_of_mode Normal = ""
   | suffix_of_mode MaSh = ""
-  | suffix_of_mode Auto_Minimize = "_min"
   | suffix_of_mode Minimize = "_min"
 
 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be
@@ -154,7 +153,7 @@
       else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix)
     val problem_file_name =
       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
-                  suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
+        suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
     val prob_path =
       if dest_dir = "" then
         File.tmp_path problem_file_name
diff -r 9f77084444df -r ee65e9cfe284 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Aug 28 16:58:27 2014 +0200
@@ -191,7 +191,7 @@
     facts =
   let
     val ctxt = Proof.context_of state
-    val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
+    val prover = get_prover ctxt Minimize prover_name
     fun test timeout = test_facts params silent prover timeout i n state goal
     val (chained, non_chained) = List.partition is_fact_chained facts
     (* Push chained facts to the back, so that they are less likely to be kicked out by the linear