# HG changeset patch
# User wenzelm
# Date 893841096 -7200
# Node ID df709de137af353337da22015142fefda29d91d2
# Parent  0afcae75b34a3bcd133afeca174d45f7187f97ce
added thm, thms;

diff -r 0afcae75b34a -r df709de137af src/Pure/Thy/context.ML
--- a/src/Pure/Thy/context.ML	Wed Apr 29 11:10:40 1998 +0200
+++ b/src/Pure/Thy/context.ML	Wed Apr 29 11:11:36 1998 +0200
@@ -13,6 +13,8 @@
   val get_context: unit -> theory
   val context: theory -> unit
   val reset_context: unit -> unit
+  val thm: xstring -> thm
+  val thms: xstring -> thm list
 end;
 
 signature CONTEXT =
@@ -25,7 +27,7 @@
 struct
 
 
-(* session *)
+(** session **)
 
 val current_session = ref ([]: string list);
 
@@ -34,7 +36,8 @@
 fun reset_session () = current_session := [];
 
 
-(* theory context *)
+
+(** theory context **)
 
 val current_theory = ref (None: theory option);
 
@@ -47,10 +50,18 @@
 fun reset_context () = current_theory := None;
 
 
+(* map context *)
+
 nonfix >>;
 fun >> f = current_theory := Some (f (get_context ()));
 
 
+(* retrieve thms *)
+
+fun thm name = PureThy.get_thm (get_context ()) name;
+fun thms name = PureThy.get_thms (get_context ()) name;
+
+
 end;