--- a/no_shm_selinux/Alive_prop.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Alive_prop.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -6,8 +6,7 @@
 
 lemma distinct_queue_msgs:
   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> distinct (msgs_of_queue s q)"
-apply (induct s)
-apply (simp add:init_msgs_distinct)
+apply (induct s, simp)
 apply (frule vd_cons, frule vt_grant_os, case_tac a)
 apply auto
 apply (case_tac "msgs_of_queue s q", simp+)