# HG changeset patch
# User desharna
# Date 1605793609 -3600
# Node ID 5f7d86b28ffb2062f96bbb6f44d25ea8a6bc0477
# Parent  febfb98d09418c00d048598428fb49066804c29b
repaired thf output broken by c7e2a9bdc585

diff -r febfb98d0941 -r 5f7d86b28ffb src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 19 14:43:50 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 19 14:46:49 2020 +0100
@@ -1109,15 +1109,14 @@
     fun intro top_level args (IApp (tm1, tm2)) =
         IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
       | intro top_level args (IConst (name as (s, _), T, T_args)) =
-        (* is_type_enc_fool *)
         (case proxify_const s of
           SOME proxy_base =>
           let
             val argc = length args
             val plain_const = IConst (name, T, [])
             fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args)
-            fun if_card_matches card x = if card = argc then x else plain_const
             val is_fool = is_type_enc_fool type_enc
+            fun if_card_matches card x = if not is_fool orelse card = argc then x else plain_const
           in
             if top_level orelse is_fool orelse is_type_enc_higher_order type_enc then
               (case (top_level, s) of
diff -r febfb98d0941 -r 5f7d86b28ffb src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Nov 19 14:43:50 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Nov 19 14:46: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_Without_Choice), "mono_native_higher_fool")
+           (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher")
          else
            (TFF (Without_FOOL, Monomorphic), "mono_native")
      in