diff -r fc7151df7f8e -r 002c34a6ff4f Dynamic_static.thy
--- a/Dynamic_static.thy	Wed Nov 20 13:44:32 2013 +0800
+++ b/Dynamic_static.thy	Wed Nov 20 15:19:58 2013 +0800
@@ -119,7 +119,7 @@
 
 lemma enrich_inherit_fds_check:
   assumes grant: "inherit_fds_check s (up, nr, nt) p fds"  and vd: "valid s"
-  and fd2sfd: "\<forall> fd. fd \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
+  and cp2sp: "\<forall> p. p  \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
   and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'"
   and fd_in: "fds \<subseteq> current_proc_fds s p" and fd_in': "fds \<subseteq> current_proc_fds s' p"
   shows "inherit_fds_check s' (up, nr, nt) p fds"