diff -r 5f86fb3ddd44 -r 811e3028d169 Static.thy
--- a/Static.thy	Tue Nov 19 09:27:25 2013 +0800
+++ b/Static.thy	Tue Nov 19 12:31:56 2013 +0800
@@ -549,8 +549,8 @@
 where
   "search_check_s pctxt sf if_file = 
     (if if_file 
-      then search_check_file pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf)
-      else search_check_dir  pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf))"
+      then search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) True
+      else search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) False)"
 
 definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set"
 where
@@ -558,8 +558,7 @@
 
 definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool"
 where
-  "inherit_fds_check_s pctxt sfds \<equiv> 
-     (\<forall> ctxt \<in> sectxts_of_sfds sfds. permission_check pctxt ctxt C_fd P_inherit)"
+  "inherit_fds_check_s pctxt sfds \<equiv> inherit_fds_check_ctxt pctxt (sectxts_of_sfds sfds)"
 
 definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set"
 where
@@ -567,8 +566,7 @@
 
 definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool"
 where
-  "inherit_shms_check_s pctxt sshms \<equiv> 
-     (\<forall> ctxt \<in> sectxts_of_sproc_sshms sshms. permission_check pctxt ctxt C_shm P_inherit)"
+  "inherit_shms_check_s pctxt sshms \<equiv> inherit_shms_check_ctxt pctxt (sectxts_of_sproc_sshms sshms)"
 
 (*
 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"