--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Apr 11 14:01:17 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Apr 13 16:53:46 2022 +0200
@@ -172,8 +172,8 @@
{exec = (["E_HOME"], ["eprover-ho", "eprover"]),
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem =>
["--tstp-in --tstp-out --silent " ^ extra_options ^
- " --demod-under-lambda=true --cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
- " --proof-object=1 " ^ File.bash_path problem],
+ " --cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^
+ File.bash_path problem],
proof_delims =
[("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
tstp_proof_delims,
@@ -186,7 +186,7 @@
let
val (format, type_enc, lam_trans, extra_options) =
if string_ord (getenv "E_VERSION", "2.7") <> LESS then
- (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true")
+ (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true")
else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule")
else