--- a/del_vs_del_s.thy	Sat Dec 14 13:07:41 2013 +1100
+++ b/del_vs_del_s.thy	Thu Dec 25 15:54:08 2014 +0000
@@ -139,7 +139,7 @@
   with exp initp vs' obtain r fr pt u 
     where SP: "obj2sobj s' (Proc p) = SProc (r,fr,pt,u) (Some p)"
     apply (frule_tac current_proc_has_sobj, simp)
-    by (simp add:obj2sobj.simps split:option.splits, blast)
+    by (simp add:obj2sobj.simps split:option.splits)
   with exp vs' all_sobjs_I[where s = s' and obj = "Proc p"]
   have SP_in: "SProc (r,fr,pt,u) (Some p) \<in> all_sobjs" by simp