# HG changeset patch
# User desharna
# Date 1608122389 -3600
# Node ID 590608c05386815e616296d8dfd60ac6b7cc3d02
# Parent  3c8d60f1dc53f471dec53ee8d54ed903875a75b4
enabled FOOL for E

diff -r 3c8d60f1dc53 -r 590608c05386 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Dec 16 09:59:15 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Dec 16 13:39:49 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_Lambda_Free), "mono_native_higher")
+           (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher_fool")
          else
            (TFF (Without_FOOL, Monomorphic), "mono_native")
      in