--- a/Flask.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Flask.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -1387,12 +1387,12 @@
 fun tobj_in_init :: "t_object \<Rightarrow> bool"
 where
   "tobj_in_init (O_proc p) = (p \<in> init_procs)"
-| "tobj_in_init (O_file f) = (f \<in> init_files)"
+| "tobj_in_init (O_file f) = (is_init_file f)"
 (* directory is not taintable 
 | "tobj_in_init (O_dir  f) = (f \<in> init_files)"
 *)
 | "tobj_in_init (O_node n) = (n \<in> init_nodes)"
-| "tobj_in_init (O_msg q m) = (member (init_msgs_of_queue q) ((op =) m))"
+| "tobj_in_init (O_msg q m) = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
 | "tobj_in_init _ = False" (* other kind of obj cannot be tainted *)
 
 (* no use