--- a/src/HOL/Unix/Unix.thy Sun Oct 14 20:06:13 2001 +0200
+++ b/src/HOL/Unix/Unix.thy Sun Oct 14 20:07:11 2001 +0200
@@ -696,7 +696,7 @@
xs_y: "r =(xs @ [y])\<Rightarrow> root''"
by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
from xs_y hyp obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
- by (auto simp add: can_exec_def)
+ by (unfold can_exec_def) blast
from x xs have "root =(x # xs)\<Rightarrow> root'"
by (rule transitions.cons)
with y show ?thesis by blast