src/HOL/Tools/res_atp.ML
changeset 26278 f0c6839df608
parent 25761 466e714de2fc
child 26501 494f418cc51c
--- a/src/HOL/Tools/res_atp.ML	Sat Mar 15 18:07:58 2008 +0100
+++ b/src/HOL/Tools/res_atp.ML	Sat Mar 15 18:07:59 2008 +0100
@@ -475,11 +475,12 @@
     val thy = ProofContext.theory_of ctxt;
     val all_thys = thy :: Theory.ancestors_of thy;
 
+    val local_facts = ProofContext.facts_of ctxt;
+
     fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab [];
   in
     maps (dest_valid o PureThy.theorems_of) all_thys @
-    fold (extern_valid (#1 (ProofContext.theorems_of ctxt)))
-      (FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])) []
+    fold (extern_valid (Facts.space_of local_facts)) (Facts.dest local_facts) []
   end;
 
 fun multi_name a (th, (n,pairs)) =