# HG changeset patch
# User wenzelm
# Date 1208375579 -7200
# Node ID 520c99e0b9a0b780c63935b82b18963bcea9504e
# Parent  e30b8d500c7d392e26ec322d00bd0bdb650c79f9
valid_facts: more elementary version using Facts.fold_static;

diff -r e30b8d500c7d -r 520c99e0b9a0 src/HOL/Tools/res_atp.ML
--- 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