--- a/Implementation.thy	Mon Mar 21 14:41:40 2016 +0000
+++ b/Implementation.thy	Mon Mar 21 15:06:52 2016 +0000
@@ -29,7 +29,7 @@
     from tranclD[OF this]
     obtain z where "(Th th, z) \<in> RAG s" by auto
     with assms(1) have False
-         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
+         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_raw)
          by (fold wq_def, blast)
   } thus ?thesis by (unfold root_def, auto)
 qed
@@ -668,7 +668,7 @@
   have "Th th \<notin> Range (RAG s)"
   proof
     assume "Th th \<in> Range (RAG s)"
-    then obtain cs where "holding (wq s) th cs"
+    then obtain cs where "holding_raw (wq s) th cs"
       by (unfold Range_iff s_RAG_def, auto)
     with holdents_th_s[unfolded holdents_def]
     show False by (unfold holding_eq, auto)
@@ -676,7 +676,7 @@
   moreover have "Th th \<notin> Domain (RAG s)"
   proof
     assume "Th th \<in> Domain (RAG s)"
-    then obtain cs where "waiting (wq s) th cs"
+    then obtain cs where "waiting_raw (wq s) th cs"
       by (unfold Domain_iff s_RAG_def, auto)
     with th_ready_s show False by (unfold readys_def waiting_eq, auto)
   qed