--- a/Flask.thy	Wed May 15 15:42:46 2013 +0800
+++ b/Flask.thy	Thu May 16 15:18:44 2013 +0800
@@ -294,10 +294,7 @@
      if (proc_fd_of_file \<tau> f = {}) 
      then (inum_of_file \<tau>) (f := None)
      else inum_of_file \<tau>            )" 
-| "inum_of_file (Rmdir p f # \<tau>) = (
-     if (proc_fd_of_file \<tau> f = {}) 
-     then (inum_of_file \<tau>) (f := None)
-     else inum_of_file \<tau>          )" 
+| "inum_of_file (Rmdir p f # \<tau>) = (inum_of_file \<tau>) (f := None)"
 | "inum_of_file (Mkdir p f ino # \<tau>) = (inum_of_file \<tau>) (f:=  Some ino)"
 | "inum_of_file (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = (inum_of_file \<tau>) (f\<^isub>2 := inum_of_file \<tau> f\<^isub>1)"
 (*
@@ -744,7 +741,7 @@
                                        deleted obj s)"
 | "deleted obj (Clone p p' fds shms # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p' fd \<and> fd \<notin> fds) \<or> 
                                             deleted obj s)"
-| "deleted obj (UnLink p f # s) = ((obj = O_file f) \<or> deleted obj s)"
+| "deleted obj (UnLink p f # s) = ((proc_fd_of_file s f = {} \<and> obj = O_file f) \<or> deleted obj s)"
 | "deleted obj (Rmdir p f # s)  = ((obj = O_dir  f) \<or> deleted obj s)"
 | "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or> 
                                (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or>