--- a/src/HOL/Unix/Unix.thy Tue Nov 07 18:14:53 2006 +0100
+++ b/src/HOL/Unix/Unix.thy Tue Nov 07 18:25:48 2006 +0100
@@ -370,7 +370,7 @@
"access root path uid {} = Some file \<Longrightarrow>
uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow>
root \<midarrow>(Chmod uid perms path)\<rightarrow> update path
- (Some (map_attributes (others_update perms) file)) root"
+ (Some (map_attributes (others_update (K_record perms)) file)) root"
creat:
"path = parent_path @ [name] \<Longrightarrow>