diff -r b84170538043 -r 1c769a2a2421 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Tue Nov 29 19:49:36 2011 +0100
+++ b/src/HOL/Unix/Unix.thy	Tue Nov 29 20:17:11 2011 +0100
@@ -450,7 +450,7 @@
   with root' show ?thesis by cases auto
 next
   case readdir
-  with root' show ?thesis by cases fastforce+
+  with root' show ?thesis by cases blast+
 qed
 
 text {*
@@ -1028,7 +1028,7 @@
             also have "\<dots> \<noteq> None"
             proof -
               from ys obtain us u where rev_ys: "ys = us @ [u]"
-                by (cases ys rule: rev_cases) fastforce+
+                by (cases ys rule: rev_cases) simp
               with tr path
               have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
                   lookup root ((path @ [y]) @ us) \<noteq> None"