Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TPTP/atp_problem_import.ML
changeset 72591 56514a42eee8
parent 72400 abfeed05c323
child 74402 e7c10f7e09fa 
--- a/src/HOL/TPTP/atp_problem_import.ML	Thu Nov 12 16:18:43 2020 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Thu Nov 12 16:42:22 2020 +0100
@@ -298,8 +298,9 @@
     val (format, type_enc, lam_trans) =
       (case format_str of
         "FOF" => (FOF, "mono_guards??", liftingN)
-      | "TF0" => (TFF Monomorphic, "mono_native", liftingN)
-      | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
+      | "TF0" => (TFF (Without_FOOL, Monomorphic), "mono_native", liftingN)
+      | "TH0" => (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher",
+        keep_lamsN)
       | "DFG" => (DFG Monomorphic, "mono_native", liftingN)
       | _ => error ("Unknown format " ^ quote format_str ^
         " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
isabelle