diff -r 11728d83794c -r 9953ff53cc64 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Unix/Unix.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -570,7 +570,7 @@
   using trans
 proof induct
   case nil
-  show ?case by assumption
+  show ?case by (rule nil.prems)
 next
   case (cons root x root' xs root'')
   note P = `\<forall>x \<in> set (x # xs). P x`