Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lthms_containing: not o valid_thms;
authorwenzelm
Fri, 28 Oct 2005 22:32:55 +0200
changeset 18043 2427edb2e8a2
parent 18042 f9890c615c0e
child 18044 f27022e2ec3a
lthms_containing: not o valid_thms;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- 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)));
isabelle