--- a/Static.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Static.thy	Wed May 15 15:42:46 2013 +0800
@@ -6,18 +6,6 @@
 
 begin
 
-fun init_role_of_obj :: "t_object \<Rightarrow> role_t option"
-where
-  "init_role_of_obj (O_proc p) = init_role_of_proc p"
-| "init_role_of_obj _          = Some R_object"
-
-definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option"
-where
-  "init_sectxt_of_obj obj \<equiv>
-     (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of
-        (Some u, Some r, Some t) \<Rightarrow> Some (u,r,t)
-      | _ \<Rightarrow> None)"
-
 (*
 definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option"
 where
@@ -27,11 +15,6 @@
      else None"
 *)
 
-definition sec_of_root :: "security_context_t"
-where
-  "sec_of_root \<equiv> (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of
-     (Some u, Some t) \<Rightarrow> (u, R_object, t))"
-
 definition sroot :: "t_sfile"
 where
   "sroot \<equiv> (Init [], sec_of_root, None, {})"