# HG changeset patch
# User wenzelm
# Date 928518926 -7200
# Node ID 175ff298ac0e8de3381a088adff34d99caf5789f
# Parent  55f1e6b639a46c55516c3a12a17c53ba171a7dee
added put_st;

diff -r 55f1e6b639a4 -r 175ff298ac0e src/Pure/Isar/proof_data.ML
--- a/src/Pure/Isar/proof_data.ML	Fri Jun 04 19:55:11 1999 +0200
+++ b/src/Pure/Isar/proof_data.ML	Fri Jun 04 19:55:26 1999 +0200
@@ -20,6 +20,7 @@
   val print: Proof.context -> unit
   val get: Proof.context -> T
   val put: T -> Proof.context -> Proof.context
+  val put_st: T -> Proof.state -> Proof.state
 end;
 
 functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
@@ -38,6 +39,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 put_st = Proof.put_data kind Data;
 
 end;