--- a/no_shm_selinux/Static.thy	Thu Jan 09 19:09:09 2014 +0800
+++ b/no_shm_selinux/Static.thy	Thu Jan 09 22:53:45 2014 +0800
@@ -702,9 +702,9 @@
 where
   "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)"
 
-definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname set"
+definition all_fname_under_dir:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_fname set"
 where
-  "all_fname_under_dir d \<tau> fs = {fn. \<exists> f. fn # d = f \<and> f \<in> (current_files \<tau> \<union> fs)}"
+  "all_fname_under_dir d fs = {fn. fn # d \<in> fs}"
 
 fun fname_all_a:: "nat \<Rightarrow> t_fname"
 where
@@ -715,17 +715,17 @@
 where
   "fname_length_set fns = length`fns"
 
-definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname"
+definition next_fname:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_fname"
 where
-  "next_fname pf \<tau> fs = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau> fs))) + 1)"
+  "next_fname pf fs = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf fs))) + 1)"
 
-definition new_childf_general:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_file"
+definition new_childf_general:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_file"
 where
-  "new_childf_general pf \<tau> fs = next_fname pf \<tau> fs # pf"
+  "new_childf_general pf fs = next_fname pf fs # pf"
 
 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file"
 where
-  "new_childf pf \<tau> = new_childf_general pf \<tau> {}"
+  "new_childf pf \<tau> = new_childf_general pf (current_files \<tau>)"
 
 end