diff -r a5dd2c966cbe -r 6a6d0bd16035 prio/ExtGG.thy
--- a/prio/ExtGG.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/ExtGG.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -461,7 +461,7 @@
 lemma th_cp_max_preced: "cp (t@s) th = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))" 
   (is "?L = ?R")
 proof -
-  have "?L = cpreced (t@s) (wq (t@s)) th" 
+  have "?L = cpreced (wq (t@s)) (t@s) th" 
     by (unfold cp_eq_cpreced, simp)
   also have "\<dots> = ?R"
   proof(unfold cpreced_def)