diff -r 572f202659ff -r 440382eb6427 prio/PrioGDef.thy
--- a/prio/PrioGDef.thy	Wed Feb 08 16:35:49 2012 +0000
+++ b/prio/PrioGDef.thy	Thu Feb 09 13:05:51 2012 +0000
@@ -159,7 +159,7 @@
   *}
   cs_depend_def: 
   "depend (wq::cs \<Rightarrow> thread list) \<equiv>
-      {(Th t, Cs c) | t c. waiting wq t c} \<union> {(Cs c, Th t) | c t. holding wq t c}"
+      {(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}"
   -- {* 
   \begin{minipage}{0.9\textwidth}
   The following @{text "dependents wq th"} represents the set of threads which are depending on
@@ -264,7 +264,7 @@
   "waiting (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"
   s_depend_def: 
   "depend (s::state) \<equiv> 
-    {(Th t, Cs c) | t c. waiting (wq s) t c} \<union> {(Cs c, Th t) | c t. holding (wq s) t c}"
+    {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}"
   s_dependents_def: 
   "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
 
@@ -273,7 +273,7 @@
   for running if it is a live thread and it is not waiting for any critical resource.
   *}
 definition readys :: "state \<Rightarrow> thread set"
-  where "readys s = {thread . thread \<in> threads s \<and> (\<forall> cs. \<not> waiting s thread cs)}"
+  where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waiting s th cs)}"
 
 text {* \noindent
   The following function @{text "runing"} calculates the set of running thread, which is the ready