# HG changeset patch
# User blanchet
# Date 1314773350 -7200
# Node ID 9eee93ead24e1a46c0a95cd464cbe01e5b11ad5c
# Parent  49e7dbaf19aa3761fba509de55cc2976bc623868
killed FIXME (the ATP exporter outputs TPTP FOF, which is first-order)

diff -r 49e7dbaf19aa -r 9eee93ead24e src/HOL/TPTP/atp_export.ML
--- a/src/HOL/TPTP/atp_export.ML	Wed Aug 31 08:49:10 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Wed Aug 31 08:49:10 2011 +0200
@@ -27,8 +27,7 @@
 val fact_name_of = prefix fact_prefix o ascii_of
 
 fun facts_of thy =
-  Sledgehammer_Filter.all_facts (Proof_Context.init_global thy)
-                                false(*FIXME works only for first-order*)
+  Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) false
                                 Symtab.empty true [] []
   |> filter (curry (op =) @{typ bool} o fastype_of
              o Object_Logic.atomize_term thy o prop_of o snd)