diff -r 4d25a9919688 -r 4294abb1f38c del_vs_del_s.thy
--- a/del_vs_del_s.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/del_vs_del_s.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -135,7 +135,7 @@
   from initp fstdel vs' have "source_proc s' p = Some p"
     apply (induct s', simp)
     apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)
-    by (case_tac a, auto dest:not_deleted_imp_exists simp:np_notin_curp)
+    by (case_tac a, auto dest:not_deleted_imp_exists)
   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)