# HG changeset patch
# User krauss
# Date 1257176658 -3600
# Node ID 81269c72321ad6323713450947a0e28ec8c8a750
# Parent  cd6023a9a922a74843f7cd87785db722b420d4b2
find_theorems: respect conceal flag

diff -r cd6023a9a922 -r 81269c72321a src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Nov 02 17:30:38 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Nov 02 16:44:18 2009 +0100
@@ -375,9 +375,15 @@
 (* print_theorems *)
 
 fun all_facts_of ctxt =
-  maps Facts.selections
-   (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @
-    Facts.dest_static [] (ProofContext.facts_of ctxt));
+  let
+    fun visible_facts facttab =
+      Facts.dest_static [] facttab
+      |> filter_out (Facts.is_concealed facttab o #1)
+  in
+    maps Facts.selections
+     (visible_facts (PureThy.facts_of (ProofContext.theory_of ctxt)) @
+      visible_facts (ProofContext.facts_of ctxt))
+  end;
 
 val limit = Unsynchronized.ref 40;