--- 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)