# HG changeset patch
# User haftmann
# Date 1242155854 -7200
# Node ID b63c3f6bd3bee5bbbc90a2ae39073d721cbcaf0d
# Parent  d8a6122affd7dc42512bda988e774a40470822fa
values is now a keyword

diff -r d8a6122affd7 -r b63c3f6bd3be src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Tue May 12 20:07:05 2009 +0200
+++ b/src/HOL/Bali/State.thy	Tue May 12 21:17:34 2009 +0200
@@ -29,7 +29,7 @@
 types	vn   = "fspec + int"                    --{* variable name      *}
 record	obj  = 
           tag :: "obj_tag"                      --{* generalized object *}
-          values :: "(vn, val) table"      
+          "values" :: "(vn, val) table"      
 
 translations 
   "fspec" <= (type) "vname \<times> qtname"