--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Nov 19 14:46:49 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Nov 19 15:11:37 2020 +0100
@@ -296,7 +296,7 @@
val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS
val (format, enc) =
if modern then
- (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher")
+ (THF (With_FOOL, Monomorphic, THF_Lambda_Bool_Free), "mono_native_higher")
else
(TFF (Without_FOOL, Monomorphic), "mono_native")
in