1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -113,10 +113,6 @@
     1.4      handle TYPE _ => @{prop True}
     1.5    end
     1.6  
     1.7 -fun all_non_tautological_facts_of thy css_table =
     1.8 -  Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
     1.9 -  |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
    1.10 -
    1.11  fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
    1.12    let
    1.13      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.14 @@ -126,7 +122,8 @@
    1.15      val mono = not (is_type_enc_polymorphic type_enc)
    1.16      val path = file_name |> Path.explode
    1.17      val _ = File.write path ""
    1.18 -    val facts = all_non_tautological_facts_of thy css_table
    1.19 +    val facts =
    1.20 +      Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
    1.21      val atp_problem =
    1.22        facts
    1.23        |> map (fn ((_, loc), th) =>