# HG changeset patch
# User wenzelm
# Date 1129751563 -7200
# Node ID e7160d70be1f32ddeb20f275ef9fc3d2007b3426
# Parent  e8d7d463436dbee3c2e357b6a374dbf622eaa11a
added thm(s) retrieval functions (from goals.ML);

diff -r e8d7d463436d -r e7160d70be1f src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Oct 19 21:52:42 2005 +0200
+++ b/src/Pure/pure_thy.ML	Wed Oct 19 21:52:43 2005 +0200
@@ -14,6 +14,8 @@
   val get_thm: theory -> thmref -> thm
   val get_thms: theory -> thmref -> thm list
   val get_thmss: theory -> thmref list -> thm list
+  val thm: xstring -> thm
+  val thms: xstring -> thm list
   structure ProtoPure:
     sig
       val thy: theory
@@ -237,6 +239,9 @@
 fun get_thmss thy thmrefs = List.concat (map (get_thms thy) thmrefs);
 fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
 
+fun thm name = get_thm (the_context ()) (Name name);
+fun thms name = get_thms (the_context ()) (Name name);
+
 
 (* thms_containing etc. *)