src/HOL/ex/tptp_export.ML

--- a/src/HOL/ex/tptp_export.ML	Mon May 02 22:31:46 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Mon May 02 22:52:15 2011 +0200
@@ -22,7 +22,7 @@
 val fact_name_of = prefix Sledgehammer_ATP_Translate.fact_prefix o ascii_of
 
 fun facts_of thy =
-  Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty true
+  Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
       true Sledgehammer_Provers.atp_relevance_fudge [] []
 
 fun fold_body_thms f =