# HG changeset patch
# User wenzelm
# Date 1208290163 -7200
# Node ID fba93ce71435dadbeb36be6e4cbef44c4fee908d
# Parent  fe93963ed76de572d0fc344379d72a49436d1cd4
all_valid_thms: use new facts tables;

diff -r fe93963ed76d -r fba93ce71435 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue Apr 15 18:49:29 2008 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Apr 15 22:09:23 2008 +0200
@@ -458,30 +458,18 @@
       filter (not o known) c_clauses
   end;
 
+fun valid_facts facts =
+  Facts.dest_table facts
+  |> filter_out (fn (name, _) => !run_blacklist_filter andalso is_package_def name)
+  |> map (apfst (Facts.extern facts))
+  |> filter_out (NameSpace.is_hidden o #1)
+  |> map (apsnd (filter_out ResAxioms.bad_for_atp));
+
 fun all_valid_thms ctxt =
   let
-    fun blacklisted s = !run_blacklist_filter andalso is_package_def s
-
-    fun extern_valid space (name, ths) =
-      let
-        val is_valid = ProofContext.valid_thms ctxt;
-        val xname = NameSpace.extern space name;
-      in
-        if blacklisted name then I
-        else if is_valid (xname, ths) then cons (xname, filter_out ResAxioms.bad_for_atp ths)
-        else if is_valid (name, ths) then cons (name, filter_out ResAxioms.bad_for_atp ths)
-        else I
-      end;
-    val thy = ProofContext.theory_of ctxt;
-    val all_thys = thy :: Theory.ancestors_of thy;
-
+    val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
     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 (Facts.space_of local_facts)) (Facts.dest_table local_facts) []
-  end;
+  in valid_facts global_facts @ valid_facts local_facts end;
 
 fun multi_name a (th, (n,pairs)) =
   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)