added Open_locale, Close_locale;
thm(s): use Locale.get_thm(s);

--- 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;