--- 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"