src/HOL/Unix/Unix.thy
changeset 21226 a607ae87ee81
parent 21029 b98fb9cf903b
child 21372 4a0a83378669
--- 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>