--- a/prio/CpsG.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/CpsG.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -276,13 +276,13 @@
 qed
 
 
-lemma cp_eq_cpreced_f: "cp s = cpreced s (wq s)"
+lemma cp_eq_cpreced_f: "cp s = cpreced (wq s) s"
 proof -
   from fun_eq_iff 
   have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto
   show ?thesis
   proof(rule h)
-    from cp_eq_cpreced show "\<forall>x. cp s x = cpreced s (wq s) x" by auto
+    from cp_eq_cpreced show "\<forall>x. cp s x = cpreced (wq s) s x" by auto
   qed
 qed