diff -r bd4e2821482a -r 7cc639e20cb2 src/HOL/Unix/Unix.thy
--- 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