# HG changeset patch
# User wenzelm
# Date 883317369 -3600
# Node ID 48e4fbc03b7c1f329150fd9fc21861f0f58819b3
# Parent  697972696f71ff7f922090914307b03af7df284b
added >> : (theory -> theory) -> unit;

diff -r 697972696f71 -r 48e4fbc03b7c src/Pure/Thy/context.ML
--- 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;