--- a/obj2sobj_prop.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/obj2sobj_prop.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -601,8 +601,7 @@
   "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; \<not> deleted (IPC i) (e#s)\<rbrakk>
   \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri"
 apply (frule valid_cons, frule valid_os, case_tac e)
-by (auto simp:ni_init_deled ni_notin_curi split:option.splits
-        dest!:current_proc_has_role')
+by (auto split:option.splits dest!:current_proc_has_role')
 
 lemma obj2sobj_ipc_remains_cons':
   "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; no_del_event (e#s)\<rbrakk>