diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -113,10 +113,6 @@
     handle TYPE _ => @{prop True}
   end
 
-fun all_non_tautological_facts_of thy css_table =
-  Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
-  |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
-
 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
   let
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
@@ -126,7 +122,8 @@
     val mono = not (is_type_enc_polymorphic type_enc)
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val facts = all_non_tautological_facts_of thy css_table
+    val facts =
+      Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
     val atp_problem =
       facts
       |> map (fn ((_, loc), th) =>