# HG changeset patch
# User wenzelm
# Date 918056791 -3600
# Node ID f0c14e527d68240d0b9719c4626b618435b7b308
# Parent  e9dc9ec28a2d8a72313cdee6d5c8907d8defffd8
added thm, thms, Open_locale, Close_locale, Print_scope;

diff -r e9dc9ec28a2d -r f0c14e527d68 src/Pure/locale.ML
--- a/src/Pure/locale.ML	Wed Feb 03 16:45:45 1999 +0100
+++ b/src/Pure/locale.ML	Wed Feb 03 16:46:31 1999 +0100
@@ -22,6 +22,11 @@
   val print_locales: theory -> unit
   val print_goals: int -> thm -> unit
   val print_goals_marker: string -> int -> thm -> unit
+  val thm: xstring -> thm
+  val thms: xstring -> thm list
+  val Open_locale: xstring -> unit
+  val Close_locale: xstring -> unit
+  val Print_scope: unit -> unit
 end;
 
 signature LOCALE =
@@ -203,6 +208,12 @@
 fun print_scope thy = 
 Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
 
+(*implicit context versions*)
+fun Open_locale xname = (open_locale xname (Context.the_context ()); ());
+fun Close_locale xname = (close_locale xname (Context.the_context ()); ());
+fun Print_scope () = (print_scope (Context.the_context ()); ());
+
+
 (** functions for goals.ML **)
 
 (* in_locale: check if hyps (: term list) of a proof are contained in the
@@ -239,8 +250,11 @@
   | None => get thy name);
 
 val get_thm = get_thmx I PureThy.get_thm;
+val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
 
-val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
+fun thm name = get_thm (Context.the_context ()) name;
+fun thms name = get_thms (Context.the_context ()) name;
+
 
 (* get the defaults of a locale, for extension *)