# HG changeset patch
# User wenzelm
# Date 936716170 -7200
# Node ID 76ed51454609818a92ea6cbd2b08c3991367ee2c
# Parent  299949eddba872c6a09a8d0c44ea713249cc5462
added context_of;

diff -r 299949eddba8 -r 76ed51454609 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Sep 07 16:55:38 1999 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Sep 07 16:56:10 1999 +0200
@@ -22,6 +22,7 @@
   val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
   val theory_of: state -> theory
   val sign_of: state -> Sign.sg
+  val context_of: state -> Proof.context
   val proof_of: state -> Proof.state
   type transition
   exception TERMINATE
@@ -140,6 +141,7 @@
   | Proof prf => g (ProofHistory.current prf));
 
 val theory_of = node_case I Proof.theory_of;
+val context_of = node_case ProofContext.init Proof.context_of;
 val sign_of = Theory.sign_of o theory_of;
 val proof_of = node_case (fn _ => raise UNDEF) I;