1.1 --- a/src/HOL/TPTP/atp_theory_export.ML Thu Jul 26 10:48:03 2012 +0200
1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Thu Jul 26 10:48:03 2012 +0200
1.3 @@ -123,7 +123,8 @@
1.4 val path = file_name |> Path.explode
1.5 val _ = File.write path ""
1.6 val facts =
1.7 - Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
1.8 + Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false
1.9 + Symtab.empty [] [] css_table
1.10 val atp_problem =
1.11 facts
1.12 |> map (fn ((_, loc), th) =>