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