diff -r a5dd2c966cbe -r 6a6d0bd16035 prio/PrioG.thy
--- a/prio/PrioG.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/PrioG.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -2071,7 +2071,7 @@
   from wq_threads [OF vt this] show ?thesis .
 qed
 
-lemma cp_eq_cpreced: "cp s th = cpreced s (wq s) th"
+lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
 proof(unfold cp_def wq_def, induct s)
   case (Cons e s')
   show ?case