src/HOL/TPTP/atp_theory_export.ML
changeset 49545 d443166f9520
parent 49453 3e45c98fe127
child 49731 1d2a12bb0640
     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) =>