# HG changeset patch
# User wenzelm
# Date 948835913 -3600
# Node ID b0e44ab7363152f8d90fadc8b54616e5b879aff0
# Parent  37d3b5a4ebae8bdb0396c15a5694329c3242ef3b
added map, map_st;

diff -r 37d3b5a4ebae -r b0e44ab73631 src/Pure/Isar/proof_data.ML
--- a/src/Pure/Isar/proof_data.ML	Tue Jan 25 22:28:48 2000 +0100
+++ b/src/Pure/Isar/proof_data.ML	Tue Jan 25 22:31:53 2000 +0100
@@ -20,8 +20,10 @@
   val print: Proof.context -> unit
   val get: Proof.context -> T
   val put: T -> Proof.context -> Proof.context
+  val map: (T -> T) -> Proof.context -> Proof.context
   val get_st: Proof.state -> T
   val put_st: T -> Proof.state -> Proof.state
+  val map_st: (T -> T) -> Proof.state -> Proof.state
 end;
 
 functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
@@ -40,8 +42,11 @@
 val print = ProofContext.print_data kind;
 val get = ProofContext.get_data kind (fn Data x => x);
 val put = ProofContext.put_data kind Data;
+fun map f ctxt = put (f (get ctxt)) ctxt;
+
 val get_st = get o Proof.context_of;
 val put_st = Proof.put_data kind Data;
+fun map_st f st = put_st (f (get_st st)) st;
 
 end;