replaced obsolete FactIndex.T by Facts.T;
authorwenzelm
Sat Mar 15 18:07:59 2008 +0100 (2008-03-15)
changeset 26278f0c6839df608
parent 26277 461e11226111
child 26279 e8440c90c474
replaced obsolete FactIndex.T by Facts.T;
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sat Mar 15 18:07:58 2008 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Sat Mar 15 18:07:59 2008 +0100
     1.3 @@ -475,11 +475,12 @@
     1.4      val thy = ProofContext.theory_of ctxt;
     1.5      val all_thys = thy :: Theory.ancestors_of thy;
     1.6  
     1.7 +    val local_facts = ProofContext.facts_of ctxt;
     1.8 +
     1.9      fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab [];
    1.10    in
    1.11      maps (dest_valid o PureThy.theorems_of) all_thys @
    1.12 -    fold (extern_valid (#1 (ProofContext.theorems_of ctxt)))
    1.13 -      (FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])) []
    1.14 +    fold (extern_valid (Facts.space_of local_facts)) (Facts.dest local_facts) []
    1.15    end;
    1.16  
    1.17  fun multi_name a (th, (n,pairs)) =