--- a/no_shm_selinux/Co2sobj_prop.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Co2sobj_prop.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -80,9 +80,11 @@
 lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'
   cm2smsg_removemsgq cm2smsg_other
 
+(*
 lemma init_cm2smsg_has_smsg:
   "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm"
 by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt)
+*)
 
 lemma hd_set_prop1:
   "hd l \<notin> set l \<Longrightarrow> l = []"
@@ -262,7 +264,7 @@
 apply (frule vd_cons, frule vt_grant_os)
 apply (frule cqm2sms_createmsgq)
 apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq 
-  split:option.splits if_splits dest:not_died_init_msgq)
+  split:option.splits if_splits)
 done
 
 lemma cq2smsg_sendmsg: