--- 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)