--- a/Static.thy	Wed Aug 28 08:59:12 2013 +0800
+++ b/Static.thy	Thu Aug 29 10:01:24 2013 +0800
@@ -592,7 +592,9 @@
                S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss;
                permission_check pctxt qctxt C_msgq P_read; 
                permission_check pctxt mctxt C_msg  P_receive\<rbrakk>
-  \<Longrightarrow> (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) \<in> static"
+  \<Longrightarrow> (update_ss (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) 
+                 (S_msgq (qi, qctxt, (mi, mctxt, tagm)#sms))
+                 (S_msgq (qi, qctxt, sms))) \<in> static"
 | s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
                permission_check pctxt qctxt C_msgq P_destroy\<rbrakk>
   \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static"
@@ -786,10 +788,12 @@
      (case (ch2sshm s h) of 
         Some sh \<Rightarrow> Some (S_shm sh)
       | _ \<Rightarrow> None)"
+(*
 | "co2sobj s (O_msg q m) = 
      (case (cq2smsgq s q, cm2smsg s q m) of 
        (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
      | _ \<Rightarrow> None)"
+*)
 | "co2sobj s _ = None"