export context_node;

--- a/src/Pure/Isar/toplevel.ML	Thu Dec 11 17:04:46 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 11 17:31:23 2008 +0100
@@ -13,6 +13,7 @@
   val theory_node: node -> generic_theory option
   val proof_node: node -> ProofNode.T option
   val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
+  val context_node: node -> Proof.context
   val presentation_context: node option -> xstring option -> Proof.context
   type state
   val toplevel: state
@@ -140,8 +141,10 @@
   | cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf)
   | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
 
+val context_node = cases_node Context.proof_of Proof.context_of;
+
 fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt
-  | presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node
+  | presentation_context (SOME node) NONE = context_node node
   | presentation_context (SOME node) (SOME loc) =
       loc_init loc (cases_node Context.theory_of Proof.theory_of node)
   | presentation_context NONE _ = raise UNDEF;