src/Pure/Isar/proof_context.ML
changeset 26361 7946f459c6c8
parent 26346 17debd2fff8e
child 26393 42febbed5460
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 20 12:09:22 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 20 16:04:30 2008 +0100
     1.3 @@ -792,6 +792,8 @@
     1.4  
     1.5  (* get_thm(s) *)
     1.6  
     1.7 +local
     1.8 +
     1.9  fun retrieve_thms _ pick ctxt (Facts.Fact s) =
    1.10        let
    1.11          val prop = Syntax.read_prop (set_mode mode_default ctxt) s
    1.12 @@ -814,19 +816,22 @@
    1.13              | NONE => from_thy thy xthmref);
    1.14        in pick name thms end;
    1.15  
    1.16 -val get_fact_silent = retrieve_thms PureThy.get_fact_silent (K I);
    1.17 +in
    1.18  
    1.19  val get_fact = retrieve_thms PureThy.get_fact (K I);
    1.20  val get_fact_single = retrieve_thms PureThy.get_fact Facts.the_single;
    1.21  
    1.22 -fun get_thms ctxt name = get_fact ctxt (Facts.Named (name, NONE));
    1.23 -fun get_thm ctxt name = get_fact_single ctxt (Facts.Named (name, NONE));
    1.24 +fun get_thms_silent ctxt = retrieve_thms PureThy.get_fact_silent (K I) ctxt o Facts.named;
    1.25 +fun get_thms ctxt = get_fact ctxt o Facts.named;
    1.26 +fun get_thm ctxt = get_fact_single ctxt o Facts.named;
    1.27 +
    1.28 +end;
    1.29  
    1.30  
    1.31  (* valid_thms *)
    1.32  
    1.33  fun valid_thms ctxt (name, ths) =
    1.34 -  (case try (fn () => get_fact_silent ctxt (Facts.Named (name, NONE))) () of
    1.35 +  (case try (fn () => get_thms_silent ctxt name) () of
    1.36      NONE => false
    1.37    | SOME ths' => Thm.eq_thms (ths, ths'));
    1.38