src/Pure/theory_data.ML

--- a/src/Pure/theory_data.ML	Tue Jan 25 20:22:57 2000 +0100
+++ b/src/Pure/theory_data.ML	Tue Jan 25 22:28:48 2000 +0100
@@ -24,6 +24,7 @@
   val get_sg: Sign.sg -> T
   val get: theory -> T
   val put: T -> theory -> theory
+  val map: (T -> T) -> theory -> theory
 end;
 
 functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
@@ -47,6 +48,7 @@
 val get_sg = Sign.get_data kind (fn Data x => x);
 val get = get_sg o Theory.sign_of;
 val put = Theory.put_data kind Data;
+fun map f thy = put (f (get thy)) thy;
 
 end;