# HG changeset patch
# User wenzelm
# Date 928607569 -7200
# Node ID 6eaf6856ee4adcca8b5823a56cfb2ba96d5da489
# Parent  25265c6807c3ad0719bf7bec3d2b65d2b19574d2
added get_st;

diff -r 25265c6807c3 -r 6eaf6856ee4a src/Pure/Isar/proof_data.ML
--- a/src/Pure/Isar/proof_data.ML	Sat Jun 05 20:32:10 1999 +0200
+++ b/src/Pure/Isar/proof_data.ML	Sat Jun 05 20:32:49 1999 +0200
@@ -20,6 +20,7 @@
   val print: Proof.context -> unit
   val get: Proof.context -> T
   val put: T -> Proof.context -> Proof.context
+  val get_st: Proof.state -> T
   val put_st: T -> Proof.state -> Proof.state
 end;
 
@@ -39,6 +40,7 @@
 val print = ProofContext.print_data kind;
 val get = ProofContext.get_data kind (fn Data x => x);
 val put = ProofContext.put_data kind Data;
+val get_st = get o Proof.context_of;
 val put_st = Proof.put_data kind Data;
 
 end;