--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 10:01:50 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100
@@ -42,8 +42,8 @@
compress : real option,
try0 : bool,
smt_proofs : bool,
- slice : bool,
minimize : bool,
+ slice : Time.time,
timeout : Time.time,
preplay_timeout : Time.time,
expect : string}
@@ -139,8 +139,8 @@
compress : real option,
try0 : bool,
smt_proofs : bool,
- slice : bool,
minimize : bool,
+ slice : Time.time,
timeout : Time.time,
preplay_timeout : Time.time,
expect : string}
@@ -173,8 +173,8 @@
compress = #compress params,
try0 = #try0 params,
smt_proofs = #smt_proofs params,
+ minimize = #minimize params,
slice = #slice params,
- minimize = #minimize params,
timeout = #timeout params,
preplay_timeout = #preplay_timeout params,
expect = #expect params}