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.
valid_thms: get_thms_silent;
authorwenzelm
Tue, 18 Mar 2008 21:57:36 +0100
changeset 26321 d875e70a94de
parent 26320 5fe18f9493ef
child 26322 eaf634e975fa
valid_thms: get_thms_silent;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 18 21:57:35 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 18 21:57:36 2008 +0100
@@ -814,12 +814,13 @@
 
 val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm;
 val get_thms = retrieve_thms PureThy.get_thms (K I);
+val get_thms_silent = retrieve_thms PureThy.get_thms_silent (K I);
 
 
 (* valid_thms *)
 
 fun valid_thms ctxt (name, ths) =
-  (case try (fn () => get_thms ctxt (Name name)) () of
+  (case try (fn () => get_thms_silent ctxt (Name name)) () of
     NONE => false
   | SOME ths' => Thm.eq_thms (ths, ths'));
isabelle