diff -r ced0fcfbcf8e -r e2c6af3ccb0d Static.thy
--- a/Static.thy	Thu Jun 06 08:00:20 2013 +0800
+++ b/Static.thy	Thu Jun 06 12:38:44 2013 +0800
@@ -653,7 +653,7 @@
   "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"
 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"
 | "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = 
-     (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,sec,tag) \<in> set sms \<and> tag = True)"
+     (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)"
 | "tainted_s ss _ = False"
 
 (*