--- a/no_shm_selinux/Flask.thy Tue Dec 17 13:30:21 2013 +0800
+++ b/no_shm_selinux/Flask.thy Wed Dec 18 10:44:36 2013 +0800
@@ -1378,7 +1378,7 @@
Some pf \<Rightarrow>
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of
(Some (pu,pr,pt), Some (du,dr,dt)) \<Rightarrow>
- (search_check s (pu,pr,pt) f \<and>
+ (search_check s (pu,pr,pt) pf \<and>
permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \<and>
permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name)
| _ \<Rightarrow> False)