diff -r 5eebea8f359f -r 3da4543034e7 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Thu Jan 25 15:31:31 2001 +0100
+++ b/src/HOL/Unix/Unix.thy	Fri Jan 26 00:14:25 2001 +0100
@@ -1064,7 +1064,7 @@
         with tr uid inv4 changed obtain file where
             "root' = update (path_of x) (Some file) root"
           by cases auto
-        with parent lookup have "lookup root' path = Some (Env att (dir(y\<mapsto>file)))"
+        with lookup parent have "lookup root' path = Some (Env att (dir(y\<mapsto>file)))"
           by (simp only: update_append_some update_cons_nil_env)
         moreover have "dir(y\<mapsto>file) \<noteq> empty" by simp
         ultimately show ?thesis ..