--- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200
@@ -61,8 +61,8 @@
fun all_facts_of_theory thy =
let val ctxt = Proof_Context.init_global thy in
- Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] []
- (Sledgehammer_Filter.clasimpset_rule_table_of ctxt)
+ Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] []
+ (Sledgehammer_Fact.clasimpset_rule_table_of ctxt)
|> rev (* try to restore the original order of facts, for MaSh *)
end