--- a/Static.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/Static.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -116,11 +116,11 @@
 | "init_obj2sobj (O_shm h) = 
      (case (init_ch2sshm h) of 
        Some sh \<Rightarrow> Some (S_shm sh)
-     | _       \<Rightarrow> None)"
+     | _       \<Rightarrow> None)"  (*
 | "init_obj2sobj (O_msg q m) = 
      (case (init_cq2smsgq q, init_cm2smsg q m) of 
         (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
-      | _                  \<Rightarrow> None)"
+      | _                  \<Rightarrow> None)" *)
 | "init_obj2sobj _ = None"
 
 definition