diff -r 9dfc8c72565a -r 13bba99ca090 Static.thy
--- a/Static.thy	Tue Sep 03 09:31:40 2013 +0800
+++ b/Static.thy	Wed Sep 04 09:07:39 2013 +0800
@@ -101,10 +101,10 @@
 | "init_obj2sobj (O_file f) = 
      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) =
+| "init_obj2sobj (O_dir f) = 
      (case (init_cf2sfile f) of
-        Some sf \<Rightarrow> Some (S_dir sf) 
-      | _ \<Rightarrow> None)"
+           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)