valid_facts: more elementary version using Facts.fold_static;

--- a/src/HOL/Tools/res_atp.ML	Wed Apr 16 21:52:58 2008 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed Apr 16 21:52:59 2008 +0200
@@ -459,11 +459,13 @@
   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));
+  Facts.fold_static (fn (name, ths) =>
+    if !run_blacklist_filter andalso is_package_def name then I
+    else
+      let val xname = Facts.extern facts name in
+        if NameSpace.is_hidden xname then I
+        else cons (xname, filter_out ResAxioms.bad_for_atp ths)
+      end) facts [];
 
 fun all_valid_thms ctxt =
   let