--- a/no_shm_selinux/Finite_current.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Finite_current.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -94,8 +94,7 @@
 
 lemma maxium_queue:
   "valid s \<Longrightarrow> length (msgs_of_queue s q) \<le> max_queue"
-apply (induct s) 
-apply (simp add:init_msgq_valid)
+apply (induct s, simp) 
 apply (frule vt_grant_os, frule vd_cons, case_tac a, auto)
 done