src/Pure/Isar/proof_data.ML

   type T
   val init: theory -> theory
   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 =
 struct
 

     (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
 
 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;
 
 
 (*hide private data access functions*)