# HG changeset patch
# User wenzelm
# Date 1283961637 -7200
# Node ID 5a3bd2b7d0eec16525b3b86d257a92183d1525a9
# Parent  52960d359969dd09ad2ce0ab9dceed52f1ff35ed# Parent  39e0d3b86112ffa84ef86778e5a8b5ca0b894a31
merged

diff -r 52960d359969 -r 5a3bd2b7d0ee src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Wed Sep 08 16:50:24 2010 +0200
+++ b/src/HOL/Unix/Unix.thy	Wed Sep 08 18:00:37 2010 +0200
@@ -945,7 +945,7 @@
 
   from inv1 inv3 inv4 and user\<^isub>1_not_root
   have not_writable: "Writable \<notin> others att"
-    by (auto simp add: access_def split: option.splits if_splits)
+    by (auto simp add: access_def split: option.splits)
 
   show ?thesis
   proof cases
@@ -1044,8 +1044,7 @@
             qed
             finally show ?thesis .
           qed
-          with ys show ?thesis
-            by (insert that, auto simp add: update_cons_cons_env)
+          with ys show ?thesis using that by auto
         qed
         also have "dir(y\<mapsto>file') \<noteq> empty" by simp
         ultimately show ?thesis ..