diff -r e7519207c2b7 -r 19106a9975c1 CookBook/Recipes/StoringData.thy --- a/CookBook/Recipes/StoringData.thy Wed Jan 14 16:46:07 2009 +0000 +++ b/CookBook/Recipes/StoringData.thy Wed Jan 14 17:47:49 2009 +0000 @@ -16,8 +16,7 @@ *} -ML {* -local +ML{*local structure Data = GenericDataFun ( type T = int Symtab.table @@ -27,11 +26,8 @@ ) in - -val lookup = Symtab.lookup o Data.get - -fun update k v = Data.map (Symtab.update (k, v)) - + 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) *}