author | wenzelm |
Mon, 02 Nov 2009 19:56:06 +0100 | |
changeset 33382 | 7d2c6e7f91bd |
parent 33381 | 81269c72321a |
child 33383 | 12d79ece3f7e |
child 33396 | 45c5c3c51918 |
--- 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)) @