--- a/prio/ExtGG.thy	Sun Feb 12 15:05:57 2012 +0000
+++ b/prio/ExtGG.thy	Sun Feb 12 15:12:50 2012 +0000
@@ -895,7 +895,7 @@
 lemma runing_inversion_3:
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th: "th' \<noteq> th"
-  shows "(th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"
+  shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
 proof -
   from runing_inversion_2 [OF runing'] and neq_th
   show ?thesis by auto