--- a/Static.thy	Fri May 17 09:04:47 2013 +0800
+++ b/Static.thy	Tue May 21 08:01:33 2013 +0800
@@ -712,7 +712,7 @@
 
 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
 where
-  "cpfd2sfds s p \<equiv> {sfd. \<exists> fd sfd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}"
+  "cpfd2sfds s p \<equiv> {sfd. \<exists> fd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}"
 
 definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
 where
@@ -723,7 +723,7 @@
 
 definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
 where
-  "cph2spshs s p \<equiv> {(sh, flag) | sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
+  "cph2spshs s p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
 
 definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
 where