--- a/Static.thy	Tue May 21 08:01:33 2013 +0800
+++ b/Static.thy	Tue May 21 10:19:51 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 sfd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}"
+  "init_cfds2sfds p \<equiv> { sfd. \<exists> fd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}"
 
 definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option"
 where
@@ -58,7 +58,7 @@
 definition init_cph2spshs 
   :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set"
 where
-  "init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> 
+  "init_cph2spshs p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> init_procs_of_shm h \<and> 
                                              init_ch2sshm h = Some sh}"
 
 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option"