diff -r 9b42765ce554 -r ced0fcfbcf8e Static.thy
--- a/Static.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Static.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -640,12 +640,12 @@
 *)
 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool"
 where
-  "init_obj_related (S_proc (Init p, sec, fds, shms) tag) (O_proc p') = (p = p')"
+  "init_obj_related (S_proc (pi, sec, fds, shms) tag) (O_proc p') = (pi = Init p')"
 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)"
 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)"
-| "init_obj_related (S_msgq (Init q, sec, sms)) (O_msgq q') = (q = q')"
-| "init_obj_related (S_shm (Init h, sec)) (O_shm h') = (h = h')"
-| "init_obj_related (S_msg (Init q, sec, sms) (Init m, secm, tagm)) (O_msg q' m') = (q = q' \<and> m = m')"
+| "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')"
+| "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')"
+| "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')"
 | "init_obj_related _ _ = False"
 
 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"