added >> : (theory -> theory) -> unit;

--- a/src/Pure/Thy/context.ML	Sun Dec 28 14:55:34 1997 +0100
+++ b/src/Pure/Thy/context.ML	Sun Dec 28 14:56:09 1997 +0100
@@ -5,7 +5,7 @@
 Global contexts: session and theory.
 *)
 
-signature CONTEXT =
+signature BASIC_CONTEXT =
 sig
   val get_session: unit -> string list
   val add_session: string -> unit
@@ -15,6 +15,12 @@
   val reset_context: unit -> unit
 end;
 
+signature CONTEXT =
+sig
+  include BASIC_CONTEXT
+  val >> : (theory -> theory) -> unit
+end;
+
 structure Context: CONTEXT =
 struct
 
@@ -41,6 +47,12 @@
 fun reset_context () = current_theory := None;
 
 
+nonfix >>;
+fun >> f = current_theory := Some (f (get_context ()));
+
+
 end;
 
-open Context;
+
+structure BasicContext: BASIC_CONTEXT = Context;
+open BasicContext;