# HG changeset patch
# User wenzelm
# Date 1205873856 -3600
# Node ID d875e70a94de1ef726bbc21e1c6403ade2f65472
# Parent  5fe18f9493eff6ef85f923e8e40e7c5ca6e09666
valid_thms: get_thms_silent;

diff -r 5fe18f9493ef -r d875e70a94de src/Pure/Isar/proof_context.ML
--- 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'));