# HG changeset patch
# User wenzelm
# Date 1257188166 -3600
# Node ID 7d2c6e7f91bd07cbacdc3ddcd6e2424c78f75be9
# Parent  81269c72321ad6323713450947a0e28ec8c8a750
observe usual naming conventions;

diff -r 81269c72321a -r 7d2c6e7f91bd src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Nov 02 16:44:18 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Nov 02 19:56:06 2009 +0100
@@ -376,9 +376,9 @@
 
 fun all_facts_of ctxt =
   let
-    fun visible_facts facttab =
-      Facts.dest_static [] facttab
-      |> filter_out (Facts.is_concealed facttab o #1)
+    fun visible_facts facts =
+      Facts.dest_static [] facts
+      |> filter_out (Facts.is_concealed facts o #1);
   in
     maps Facts.selections
      (visible_facts (PureThy.facts_of (ProofContext.theory_of ctxt)) @