src/HOL/Unix/Unix.thy

 next
   case rmdir
   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 {*
   \medskip Apparently, file-system transitions are \emph{type-safe} in
   the sense that the result of transforming an actual directory yields

             also from lookup have "\<dots> = lookup root (path @ [y])"
               by (simp only: lookup_append_some)
             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"
                 by cases (auto dest: access_some_lookup)
               then show ?thesis