# HG changeset patch
# User wenzelm
# Date 1136918021 -3600
# Node ID 688056d430b008783d11119546e56bf941441e30
# Parent  61627ae3ddc3e38621031848aa9242d0932943ec
added context_of -- generic context;

diff -r 61627ae3ddc3 -r 688056d430b0 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jan 10 19:33:39 2006 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Jan 10 19:33:41 2006 +0100
@@ -21,6 +21,7 @@
   val node_history_of: state -> node History.T
   val node_of: state -> node
   val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
+  val context_of: state -> Context.generic
   val theory_of: state -> theory
   val sign_of: state -> theory    (*obsolete*)
   val body_context_of: state -> Proof.context
@@ -163,6 +164,7 @@
   | Proof (prf, _) => g (ProofHistory.current prf)
   | SkipProof ((_, thy), _) => f thy);
 
+val context_of = node_case Context.Theory (Context.Proof o Proof.context_of);
 val theory_of = node_case I Proof.theory_of;
 val sign_of = theory_of;