# HG changeset patch
# User wenzelm
# Date 881239818 -3600
# Node ID ab73573067d6af3a559f113aff21b6b8dd251613
# Parent  b449831f03f47dcc112f1529aaee30c8c7ab3250
added reset_context;

diff -r b449831f03f4 -r ab73573067d6 src/Pure/Thy/context.ML
--- a/src/Pure/Thy/context.ML	Thu Dec 04 13:49:51 1997 +0100
+++ b/src/Pure/Thy/context.ML	Thu Dec 04 13:50:18 1997 +0100
@@ -12,6 +12,7 @@
   val reset_session: unit -> unit
   val get_context: unit -> theory
   val context: theory -> unit
+  val reset_context: unit -> unit
 end;
 
 structure Context: CONTEXT =
@@ -29,10 +30,15 @@
 
 (* theory context *)
 
-val current_theory = ref ProtoPure.thy;
+val current_theory = ref (None: theory option);
 
-fun context thy = current_theory := thy;
-fun get_context () = ! current_theory;
+fun get_context () =
+  (case current_theory of
+    ref (Some thy) => thy
+  | _ => error "Unknown theory context");
+
+fun context thy = current_theory := Some thy;
+fun reset_context () = current_theory := None;
 
 
 end;