removed Thy;
authorwenzelm
Thu, 18 Jun 1998 11:22:45 +0200
changeset 5049 bde086cfa597
parent 5048 2af6b01e7ab6
child 5050 e925308df78b
removed Thy; the_context made public;
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;