diff -r 042e1e7fd505 -r b7fd75d104bf no_shm_selinux/Enrich.thy
--- a/no_shm_selinux/Enrich.thy	Thu Jan 09 22:53:45 2014 +0800
+++ b/no_shm_selinux/Enrich.thy	Thu Jan 16 11:04:04 2014 +0800
@@ -51,14 +51,6 @@
 | "all_inums (Accept p fd addr lport fd' i # s) = (all_inums s \<union> {i})"
 | "all_inums (_ # s) = all_inums s"
 
-fun all_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"
-where
-  "all_fds [] = init_fds_of_proc"
-| "all_fds (Open p f flags fd ipt # s) = (all_fds s) (p := all_fds s p \<union> {fd})"
-| "all_fds (CreateSock p sf st fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})"
-| "all_fds (Accept p fd' raddr port fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})"
-| "all_fds (Clone p p' fds # s) = (all_fds s) (p' := fds)"
-| "all_fds (_ # s) = all_fds s"
 
 fun all_msgqs:: "t_state \<Rightarrow> t_msgq set"
 where