diff -r 35a2ac83a262 -r 0c8a9c028304 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- 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