src/Pure/Thy/context.ML

--- a/src/Pure/Thy/context.ML	Fri Dec 11 10:34:03 1998 +0100
+++ b/src/Pure/Thy/context.ML	Fri Dec 11 10:36:39 1998 +0100
@@ -14,7 +14,8 @@
   val Goal: string -> thm list
   val Goalw: thm list -> string -> thm list
   val Open_locale: xstring -> unit
-  val Close_locale: unit -> unit
+  val Close_locale: xstring -> unit
+  val Print_scope: unit -> unit
   val Export: thm -> thm
 end;
 
@@ -89,7 +90,8 @@
 (* scope manipulation *)
 
 fun Open_locale xname = (Locale.open_locale xname (the_context ()); ());
-fun Close_locale () = (Locale.close_locale (the_context ()); ());
+fun Close_locale xname = (Locale.close_locale xname (the_context ()); ());
+fun Print_scope () = (Locale.print_scope (the_context()); ());
 fun Export th = export_thy (the_context ()) th;
 
 end;