src/Pure/Isar/proof_context.ML

   fact_tac (Facts.could_unify (facts_of ctxt) (Term.strip_all_body goal)) i);
 
 
 (* get_thm(s) *)
 
+local
+
 fun retrieve_thms _ pick ctxt (Facts.Fact s) =
       let
         val prop = Syntax.read_prop (set_mode mode_default ctxt) s
           |> singleton (Variable.polymorphic ctxt);
         val th = Goal.prove ctxt [] [] prop (K (ALLGOALS (some_fact_tac ctxt)))

             (case Facts.lookup local_facts name of
               SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
             | NONE => from_thy thy xthmref);
       in pick name thms end;
 
-val get_fact_silent = retrieve_thms PureThy.get_fact_silent (K I);
+in
 
 val get_fact = retrieve_thms PureThy.get_fact (K I);
 val get_fact_single = retrieve_thms PureThy.get_fact Facts.the_single;
 
-fun get_thms ctxt name = get_fact ctxt (Facts.Named (name, NONE));
-fun get_thm ctxt name = get_fact_single ctxt (Facts.Named (name, NONE));
+fun get_thms_silent ctxt = retrieve_thms PureThy.get_fact_silent (K I) ctxt o Facts.named;
+fun get_thms ctxt = get_fact ctxt o Facts.named;
+fun get_thm ctxt = get_fact_single ctxt o Facts.named;
+
+end;
 
 
 (* valid_thms *)
 
 fun valid_thms ctxt (name, ths) =
-  (case try (fn () => get_fact_silent ctxt (Facts.Named (name, NONE))) () of
+  (case try (fn () => get_thms_silent ctxt name) () of
     NONE => false
   | SOME ths' => Thm.eq_thms (ths, ths'));
 
 
 (* name space operations *)