--- a/PrioGDef.thy	Tue May 06 14:36:40 2014 +0100
+++ b/PrioGDef.thy	Thu May 15 16:02:44 2014 +0100
@@ -190,8 +190,9 @@
   @{text "th"}'s {\em current precedence} equals its original precedence, i.e. 
   @{text "preced th s"}.
   *}
+
 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
-  where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependants wq th)))"
+  where "cpreced wq s = (\<lambda>th. Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants wq th)))"
 
 (*<*)
 lemma