--- a/Static.thy	Tue May 21 10:19:51 2013 +0800
+++ b/Static.thy	Wed May 22 15:22:50 2013 +0800
@@ -47,7 +47,7 @@
 
 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set"
 where
-  "init_cfds2sfds p \<equiv> { sfd. \<exists> fd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}"
+  "init_cfds2sfds p \<equiv> { sfd. \<exists> fd \<in> init_proc_file_fds p. init_cfd2sfd p fd = Some sfd}"
 
 definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option"
 where
@@ -712,7 +712,7 @@
 
 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
 where
-  "cpfd2sfds s p \<equiv> {sfd. \<exists> fd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}"
+  "cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}"
 
 definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
 where