diff -r bea94f1e6771 -r dae7501b26ac prio/ExtGG.thy
--- a/prio/ExtGG.thy	Fri Apr 20 11:45:06 2012 +0000
+++ b/prio/ExtGG.thy	Fri Apr 20 14:15:36 2012 +0000
@@ -601,9 +601,11 @@
     have in_thread: "th' \<in> threads (t @ s)"
       and not_holding: "cntP (t @ s) th' = cntV (t @ s) th'" by auto
     from Cons have "extend_highest_gen s th prio tm t" by auto
-    from extend_highest_gen.pv_blocked 
-    [OF this, OF in_thread neq_th' not_holding]
-    have not_runing: "th' \<notin> runing (t @ s)" .
+    then have not_runing: "th' \<notin> runing (t @ s)" 
+      apply(rule extend_highest_gen.pv_blocked) 
+      using Cons(1) in_thread neq_th' not_holding
+      apply(simp_all add: detached_eq)
+      done
     show ?case
     proof(cases e)
       case (V thread cs)
@@ -751,15 +753,16 @@
         next
           from red_moment show "extend_highest_gen s th prio tm (moment (i + k) t)" .
         next
-          from Suc show "cntP (moment (i + k) t @ s) th' = cntV (moment (i + k) t @ s) th'"
-            by (auto)
+          from Suc vt_e show "detached (moment (i + k) t @ s) th'"
+            apply(subst detached_eq)
+            apply(auto intro: vt_e evt_cons)
+            done
         qed
       qed
       from step_back_step[OF vt_e]
       have "step ((moment (i + k) t)@s) e" .
       hence "cntP (e#(moment (i + k) t)@s) th' = cntV (e#(moment (i + k) t)@s) th' \<and>
-        th' \<in> threads (e#(moment (i + k) t)@s)
-        "
+        th' \<in> threads (e#(moment (i + k) t)@s)"
       proof(cases)
         case (thread_create thread prio)
         with Suc show ?thesis by (auto simp:cntP_def cntV_def count_def)
@@ -828,8 +831,11 @@
   from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij
   have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'"
     and h2: "th' \<in> threads ((moment j t)@s)" by auto
-  with extend_highest_gen.pv_blocked [OF  red_moment [of j], OF h2 neq_th' h1]
-  show ?thesis by auto
+  with extend_highest_gen.pv_blocked 
+  show ?thesis 
+    using  red_moment [of j] h2 neq_th' h1
+    apply(auto)
+    by (metis extend_highest_gen.pv_blocked_pre)
 qed
 
 lemma moment_blocked: