diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Recipes/StoringData.thy
--- a/CookBook/Recipes/StoringData.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Recipes/StoringData.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -7,7 +7,7 @@
 
 text {*
   {\bf Problem:} 
-  Your tool needs to keep complex data.\smallskip
+  Your tool needs to manage data.\smallskip
 
   {\bf Solution:} This can be achieved using a generic data slot.\smallskip
 
@@ -16,15 +16,15 @@
 
   *}
 
-ML {* local
+ML {* 
+local
 
 structure Data = GenericDataFun
-(
-  type T = int Symtab.table
-  val empty = Symtab.empty
-  val extend = I
-  fun merge _ = Symtab.merge (K true)
-)
+ ( type T = int Symtab.table
+   val empty = Symtab.empty
+   val extend = I
+   fun merge _ = Symtab.merge (K true)
+ )
 
 in
 
@@ -36,7 +36,12 @@
 
 setup {* Context.theory_map (update "foo" 1) *}
 
-ML {* lookup (Context.Proof @{context}) "foo" *}
+text {*
+ 
+  @{ML_response [display] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"} 
+
+
+*}
 
 text {*
   alternatives: TheoryDataFun, ProofDataFun