--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Recipes/StoringData.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,46 @@
+theory StoringData
+imports "../Base"
+begin
+
+section {* Storing Data\label{rec:storingdata} *} 
+
+
+text {*
+  {\bf Problem:} 
+  Your tool needs to manage 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) *}
+
+text {*
+ 
+  @{ML_response [display,gray] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"} 
+
+
+*}
+
+text {*
+  alternatives: TheoryDataFun, ProofDataFun
+  Code: Pure/context.ML *}
+
+end
\ No newline at end of file