--- 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"
(*