diff -r db15ef2ee18c -r 021672ec28f5 Static.thy
--- a/Static.thy	Wed Sep 04 15:13:54 2013 +0800
+++ b/Static.thy	Thu Sep 05 13:23:03 2013 +0800
@@ -167,11 +167,12 @@
 
 fun is_many :: "t_sobject \<Rightarrow> bool"
 where
-  "is_many (S_proc (Many, sec, fds, shms) tag) = True"
-| "is_many (S_file sfs                    tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
-| "is_many (S_dir  sf                        ) = is_many_sfile sf"
-| "is_many (S_msgq sq                        ) = is_many_smsgq sq"
-| "is_many (S_shm  sh                        ) = is_many_sshm  sh"
+  "is_many (S_proc sp   tag) = is_many_sproc sp"
+| "is_many (S_file sfs  tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
+| "is_many (S_dir  sf      ) = is_many_sfile sf"
+| "is_many (S_msgq sq      ) = is_many_smsgq sq"
+| "is_many (S_shm  sh      ) = is_many_sshm  sh"
+| "is_many _                 = False"
 
 (*
 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"