--- 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;