diff -r 5b9c6010897b -r 64c9540f2f84 CookBook/Recipes/StoringData.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/StoringData.thy	Wed Jan 07 16:29:49 2009 +0100
@@ -0,0 +1,47 @@
+theory StoringData
+imports "../Base"
+begin
+
+section {* Storing Data *} 
+
+
+text {*
+  {\bf Problem:} 
+  Your tool needs to keep complex data.\smallskip
+
+  {\bf Solution:} This can be achieved using a generic data slot.\smallskip
+
+  Every generic data slot may keep data of any kind which is stored in the
+  context.
+
+  *}
+
+ML {*
+local
+
+structure Data = GenericDataFun
+(
+  type T = int Symtab.table
+  val empty = Symtab.empty
+  val extend = I
+  fun merge _ = Symtab.merge (K true)
+)
+
+in
+
+val lookup = Symtab.lookup o Data.get
+
+fun update k v = Data.map (Symtab.update (k, v))
+
+end
+*}
+
+setup {* Context.theory_map (update "foo" 1) *}
+
+ML {* lookup (Context.Proof @{context}) "foo" *}
+
+text {*
+  alternatives: TheoryDataFun, ProofDataFun
+  Code: Pure/context.ML *}
+
+end
\ No newline at end of file