# HG changeset patch
# User blanchet
# Date 1649861626 -7200
# Node ID a36a1cc0144c7ef49b9b0c43381c1872d474d21c
# Parent  6b38054241b84fa9e012d5deed14030d021d5ab1
pass new option only to new version of E

diff -r 6b38054241b8 -r a36a1cc0144c src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- 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