src/HOL/TPTP/atp_theory_export.ML
changeset 48530 d443166f9520
parent 48438 3e45c98fe127
child 48716 1d2a12bb0640
--- a/src/HOL/TPTP/atp_theory_export.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -123,7 +123,8 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val facts =
-      Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
+      Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false
+                                  Symtab.empty [] [] css_table
     val atp_problem =
       facts
       |> map (fn ((_, loc), th) =>