# HG changeset patch
# User wenzelm
# Date 1205600879 -3600
# Node ID f0c6839df608c903eaece5a30bbc8b43cc9ab074
# Parent  461e11226111292b3a6d5c5736830ae97fb6e5b1
replaced obsolete FactIndex.T by Facts.T;

diff -r 461e11226111 -r f0c6839df608 src/HOL/Tools/res_atp.ML
--- 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)) =