src/HOL/Unix/Unix.thy

     root =xs\<Rightarrow> root' \<Longrightarrow> Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
 proof -
   assume r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r'"
   assume "root =xs\<Rightarrow> root'"
   thus "Q root \<Longrightarrow> (\<forall>x \<in> set xs. P x) \<Longrightarrow> Q root'" (is "PROP ?P root xs root'")
-  proof (induct ?P root xs root')
+  proof (induct root xs root')
     fix root assume "Q root"
     thus "Q root" .
   next
     fix root root' root'' and x xs
     assume root': "root \<midarrow>x\<rightarrow> root'"