diff -r 1397b2a763ab -r 029cccce84b4 Static.thy
--- a/Static.thy	Mon Sep 02 11:12:42 2013 +0800
+++ b/Static.thy	Tue Sep 03 07:25:39 2013 +0800
@@ -99,16 +99,12 @@
        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
      | _ \<Rightarrow> None)"
 | "init_obj2sobj (O_file f) = 
-     (if (f \<in> init_files \<and> is_init_file f) 
-      then Some (S_file (init_cf2sfiles f) 
-                        (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))
-      else None)"
-| "init_obj2sobj (O_dir f) = 
-     (if (is_init_dir f) then 
-        (case (init_cf2sfile f) of
-           Some sf \<Rightarrow> Some (S_dir sf) 
-         | _ \<Rightarrow> None)
-      else None)"
+     Some (S_file (init_cf2sfiles f) 
+                  (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
+| "init_obj2sobj (O_dir f) =
+     (case (init_cf2sfile f) of
+        Some sf \<Rightarrow> Some (S_dir sf) 
+      | _ \<Rightarrow> None)"
 | "init_obj2sobj (O_msgq q) = 
      (case (init_cq2smsgq q) of
        Some sq \<Rightarrow> Some (S_msgq sq)
@@ -773,9 +769,7 @@
         Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
       | _       \<Rightarrow> None)"
 | "co2sobj s (O_file f) = 
-     (if (f \<in> current_files s) then 
-        Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))
-      else None)"
+     Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
 | "co2sobj s (O_dir f) = 
      (case (cf2sfile s f) of
         Some sf  \<Rightarrow> Some (S_dir sf)