# HG changeset patch
# User wenzelm
# Date 948835728 -3600
# Node ID 37d3b5a4ebae8bdb0396c15a5694329c3242ef3b
# Parent  d6d896e81cd74438a3bc49bc56eee496eb2f0a1f
added map;

diff -r d6d896e81cd7 -r 37d3b5a4ebae 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;