--- a/source_prop.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/source_prop.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -23,7 +23,7 @@
   "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> \<Longrightarrow> source_proc s p = Some p"
 apply (induct s, simp)
 apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)
-apply (case_tac a, auto simp:np_notin_curp dest:not_deleted_imp_exists)
+apply (case_tac a, auto dest:not_deleted_imp_exists)
 done
 
 lemma init_proc_keeps_source: