# 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)) =