# HG changeset patch
# User wenzelm
# Date 898161765 -7200
# Node ID bde086cfa597810c8ffa9fcf50ea8ed0cc4945c5
# Parent  2af6b01e7ab63f4fd4e0e6e6b78bf128b0b98eb1
removed Thy;
the_context made public;

diff -r 2af6b01e7ab6 -r bde086cfa597 src/Pure/Thy/context.ML
--- a/src/Pure/Thy/context.ML	Thu Jun 18 11:20:54 1998 +0200
+++ b/src/Pure/Thy/context.ML	Thu Jun 18 11:22:45 1998 +0200
@@ -8,7 +8,7 @@
 signature BASIC_CONTEXT =
 sig
   val context: theory -> unit
-  val Thy: unit -> theory
+  val the_context: unit -> theory
   val Thm: xstring -> thm
   val Thms: xstring -> thm list
   val Goal: string -> thm list
@@ -24,7 +24,6 @@
   val welcome: unit -> string
   val get_context: unit -> theory option
   val set_context: theory option -> unit
-  val the_context: unit -> theory
   val reset_context: unit -> unit
   val >> : (theory -> theory) -> unit
 end;
@@ -62,8 +61,6 @@
     Some thy => thy
   | _ => error "Unknown theory context");
 
-val Thy = the_context;
-
 fun context thy = set_context (Some thy);
 fun reset_context () = set_context None;