diff -r f76135c6c527 -r ce754ad78bc9 ProgTutorial/Recipes/StoringData.thy
--- a/ProgTutorial/Recipes/StoringData.thy	Thu Oct 01 10:19:21 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-theory StoringData
-imports "../Base"
-begin
-
-section {* Storing Data (TBD)\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