--- a/CpsG.thy	Tue Jul 15 17:25:53 2014 +0200
+++ b/CpsG.thy	Wed Sep 09 11:24:19 2015 +0100
@@ -569,7 +569,7 @@
   from tranclD[OF this]
   obtain z where "(Th th, z) \<in> RAG s'" by auto
   with rd_th show "False"
-    apply (case_tac z, auto simp:readys_def s_waiting_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_def)
     by (fold wq_def, blast)
 qed