# HG changeset patch # User desharna # Date 1641376601 -3600 # Node ID afd8da649d75d9ee36580358be9601e4470254fe # Parent 507203e30db4f4a1ef778aee9d46964ee7a17dc3 removed $ite from E 2.6 in THF format diff -r 507203e30db4 -r afd8da649d75 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 03 13:29:05 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Jan 05 10:56:41 2022 +0100 @@ -302,7 +302,7 @@ 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) else if string_ord (getenv "E_VERSION", "2.6") <> LESS then - (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) + (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) else (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN) in