# HG changeset patch
# User blanchet
# Date 1649431041 -7200
# Node ID 9c0300345e174ad085b0c8a5b60adfe9336e0f7a
# Parent  b9c6758bb784c78ff61ce6cc9fd998a488c248af
enable an E option suggested by Petar Vukmirovic

diff -r b9c6758bb784 -r 9c0300345e17 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Apr 07 12:37:42 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Apr 08 17:17:21 2022 +0200
@@ -171,8 +171,9 @@
 val e_config : atp_config =
   {exec = (["E_HOME"], ["eprover-ho", "eprover"]),
    arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem =>
-     ["--tstp-in --tstp-out --silent " ^ extra_options ^ " --cpu-limit=" ^
-      string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path 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],
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
      tstp_proof_delims,