avoid clash with keyword 'write';

--- a/src/HOL/TLA/Memory/MemoryParameters.thy	Thu Apr 29 11:05:13 2010 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Thu Apr 29 16:53:08 2010 +0200
@@ -12,7 +12,7 @@
 begin
 
 (* the memory operations *)
-datatype memOp = read Locs | write Locs Vals
+datatype memOp = read Locs | "write" Locs Vals
 
 consts
   (* memory locations and contents *)

--- a/src/HOL/Unix/Unix.thy	Thu Apr 29 11:05:13 2010 +0200
+++ b/src/HOL/Unix/Unix.thy	Thu Apr 29 16:53:08 2010 +0200
@@ -358,7 +358,7 @@
   read:
     "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
       root \<midarrow>(Read uid text path)\<rightarrow> root" |
-  write:
+  "write":
     "access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow>
       root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root" |
 
@@ -436,7 +436,7 @@
   case read
   with root' show ?thesis by cases auto
 next
-  case write
+  case "write"
   with root' show ?thesis by cases auto
 next
   case chmod