--- a/prio/CpsG.thy	Thu Feb 16 08:12:01 2012 +0000
+++ b/prio/CpsG.thy	Mon Feb 20 11:02:50 2012 +0000
@@ -49,7 +49,7 @@
       case (thread_P thread cs)
       assume eq_e: "e = P thread cs"
       and is_runing: "thread \<in> runing s"
-      from prems have vtp: "vt (P thread cs#s)" by auto
+      from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto
       have neq_th: "th \<noteq> thread" 
       proof -
         from not_in eq_e have "th \<notin> threads s" by simp
@@ -77,7 +77,7 @@
           by (simp add:runing_def readys_def)
         ultimately show ?thesis by auto
       qed
-      from prems have vtv: "vt (V thread cs#s)" by auto
+      from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto
       from hold obtain rest 
         where eq_wq: "wq s cs = thread # rest"
         by (case_tac "wq s cs", auto simp: wq_def s_holding_def)