src/Pure/Isar/proof_context.ML
changeset 26321 d875e70a94de
parent 26309 fb52fe23acc4
child 26336 a0e2b706ce73
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 18 21:57:35 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 18 21:57:36 2008 +0100
     1.3 @@ -814,12 +814,13 @@
     1.4  
     1.5  val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm;
     1.6  val get_thms = retrieve_thms PureThy.get_thms (K I);
     1.7 +val get_thms_silent = retrieve_thms PureThy.get_thms_silent (K I);
     1.8  
     1.9  
    1.10  (* valid_thms *)
    1.11  
    1.12  fun valid_thms ctxt (name, ths) =
    1.13 -  (case try (fn () => get_thms ctxt (Name name)) () of
    1.14 +  (case try (fn () => get_thms_silent ctxt (Name name)) () of
    1.15      NONE => false
    1.16    | SOME ths' => Thm.eq_thms (ths, ths'));
    1.17