# HG changeset patch
# User wenzelm
# Date 902247874 -7200
# Node ID 9d7e6f7110ef80a7e651cac2c43f575a763ff69a
# Parent  6b04b9a88c21927bb9530252289998fd92bd8de9
added Open_locale, Close_locale;
thm(s): use Locale.get_thm(s);

diff -r 6b04b9a88c21 -r 9d7e6f7110ef src/Pure/Thy/context.ML
--- a/src/Pure/Thy/context.ML	Tue Aug 04 18:23:57 1998 +0200
+++ b/src/Pure/Thy/context.ML	Tue Aug 04 18:24:34 1998 +0200
@@ -13,6 +13,8 @@
   val thms: xstring -> thm list
   val Goal: string -> thm list
   val Goalw: thm list -> string -> thm list
+  val Open_locale: xstring -> unit
+  val Close_locale: unit -> unit
 end;
 
 signature CONTEXT =
@@ -73,8 +75,8 @@
 
 (* retrieve thms *)
 
-fun thm name = PureThy.get_thm (the_context ()) name;
-fun thms name = PureThy.get_thms (the_context ()) name;
+fun thm name = Locale.get_thm (the_context ()) name;
+fun thms name = Locale.get_thms (the_context ()) name;
 
 
 (* shortcut goal commands *)
@@ -83,6 +85,12 @@
 fun Goalw thms s = Goals.atomic_goalw (the_context ()) thms s;
 
 
+(* scope manipulation *)
+
+fun Open_locale xname = (Locale.open_locale xname (the_context ()); ());
+fun Close_locale () = (Locale.close_locale (the_context ()); ());
+
+
 end;