--- a/ExtGG.thy	Tue May 20 12:49:21 2014 +0100
+++ b/ExtGG.thy	Thu May 22 17:40:39 2014 +0100
@@ -978,7 +978,7 @@
   from th_kept have "th \<in> threads (t@s)" by auto
   from th_chain_to_ready[OF vt_t this] and not_ready
   obtain th' where th'_in: "th' \<in> readys (t@s)"
-    and dp: "(Th th, Th th') \<in> (depend (t @ s))\<^sup>+" by auto
+    and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
   have "th' \<in> runing (t@s)"
   proof -
     have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"
@@ -1021,7 +1021,7 @@
       next
         from dp
         have "th \<in> dependants (wq (t @ s)) th'" 
-          by (unfold cs_dependants_def, auto simp:eq_depend)
+          by (unfold cs_dependants_def, auto simp:eq_RAG)
         thus "preced th (t @ s) \<in> 
                 (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')"
           by auto