# 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)));