diff -r cebdef333899 -r 1d1aa5bdd37d no_shm_selinux/Co2sobj_prop.thy
--- a/no_shm_selinux/Co2sobj_prop.thy	Mon Dec 30 12:01:09 2013 +0800
+++ b/no_shm_selinux/Co2sobj_prop.thy	Mon Dec 30 14:04:23 2013 +0800
@@ -805,7 +805,7 @@
   "valid (Open p f flags fd opt # s)
    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd = 
      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
-        (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)
+        (Some sec, Some sf) \<Rightarrow> Some (sec, remove_create_flag flags, sf)
       | _ \<Rightarrow> None)"
 by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits)
 
@@ -854,7 +854,7 @@
   "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd (Open p f flags fd opt # s) p' fd' = Some f'\<rbrakk>
    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then 
      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
-        (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)
+        (Some sec, Some sf) \<Rightarrow> Some (sec, remove_create_flag flags, sf)
       | _ \<Rightarrow> None)         else cfd2sfd s p' fd')"
 apply (simp split:if_splits)
 apply (simp add:cfd2sfd_open1 split:option.splits)
@@ -1003,7 +1003,7 @@
   "valid (Open p f flags fd opt # s) \<Longrightarrow>
    cpfd2sfds (Open p f flags fd opt # s) p = (
     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
-        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
+        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, remove_create_flag flags, sf)}
       | _ \<Rightarrow> cpfd2sfds s p)"
 apply (frule cfd2sfd_open1)
 apply (auto dest:cpfd2sfds_open1 split:option.splits)
@@ -1027,7 +1027,7 @@
   "valid (Open p f flags fd opt # s)
    \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := (
     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
-        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
+        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, remove_create_flag flags, sf)}
       | _ \<Rightarrow> cpfd2sfds s p))"
 apply (rule ext)
 apply (case_tac "x \<noteq> p")
@@ -1479,7 +1479,7 @@
            cf2sfile (Open p f flags fd opt # s) f) of 
        (Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> died (O_proc p) s \<and> p \<in> init_procs) 
                                                then Init p else Created, sec, 
-                                                (cpfd2sfds s p) \<union> {(fdsec, flags, sf)})
+                                                (cpfd2sfds s p) \<union> {(fdsec, remove_create_flag flags, sf)})
      | _        \<Rightarrow> None)" (*, cph2spshs s p 
 apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp) *)
 apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext)