# HG changeset patch
# User wenzelm
# Date 1130531575 -7200
# Node ID 2427edb2e8a2430b926e74bb8e7a3853df5d5dbe
# Parent  f9890c615c0e8b186e8895632629670e832af1aa
lthms_containing: not o valid_thms;

diff -r f9890c615c0e -r 2427edb2e8a2 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Oct 28 22:28:15 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Oct 28 22:32:55 2005 +0200
@@ -975,7 +975,7 @@
 
 fun lthms_containing ctxt spec =
   FactIndex.find (fact_index_of ctxt) spec
-  |> map (valid_thms ctxt ? apfst (fn name =>
+  |> map ((not o valid_thms ctxt) ? apfst (fn name =>
     NameSpace.hidden (if name = "" then "unnamed" else name)));