--- 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
--- 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
--- 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