--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Jun 09 12:13:15 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 10 15:55:41 2020 +0200
@@ -68,7 +68,7 @@
("isar_proofs", "smart"),
("compress", "smart"),
("try0", "true"),
- ("smt_proofs", "smart"),
+ ("smt_proofs", "true"),
("slice", "true"),
("minimize", "true"),
("preplay_timeout", "1")]
@@ -267,7 +267,7 @@
val isar_proofs = lookup_option lookup_bool "isar_proofs"
val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
val try0 = lookup_bool "try0"
- val smt_proofs = lookup_option lookup_bool "smt_proofs"
+ val smt_proofs = lookup_bool "smt_proofs"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize = lookup_bool "minimize"
val timeout = lookup_time "timeout"