--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Jun 09 12:13:15 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jun 10 15:55:41 2020 +0200
@@ -36,7 +36,7 @@
isar_proofs : bool option,
compress : real option,
try0 : bool,
- smt_proofs : bool option,
+ smt_proofs : bool,
slice : bool,
minimize : bool,
timeout : Time.time,
@@ -121,7 +121,7 @@
isar_proofs : bool option,
compress : real option,
try0 : bool,
- smt_proofs : bool option,
+ smt_proofs : bool,
slice : bool,
minimize : bool,
timeout : Time.time,
@@ -155,7 +155,7 @@
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
| _ => "Try this")
-fun bunches_of_proof_methods try0 smt_method needs_full_types desperate_lam_trans =
+fun bunches_of_proof_methods try0 smt_proofs needs_full_types desperate_lam_trans =
(if try0 then
[[Simp_Method, Auto_Method, Blast_Method, Linarith_Method],
[Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]]
@@ -171,7 +171,7 @@
[Metis_Method (SOME full_typesN, NONE),
Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @
- (if smt_method then [[SMT_Method]] else [])
+ (if smt_proofs then [[SMT_Method]] else [])
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained