src/HOL/TPTP/atp_theory_export.ML

--- a/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -114,7 +114,7 @@
   end
 
 fun all_non_tautological_facts_of thy css_table =
-  Sledgehammer_Fact.all_facts_of thy css_table
+  Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
   |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd)
 
 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =