--- a/prio/PrioGDef.thy	Sat Feb 11 09:34:46 2012 +0000
+++ b/prio/PrioGDef.thy	Sat Feb 11 10:09:39 2012 +0000
@@ -198,8 +198,7 @@
   "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
   unfolding cpreced_def image_def
   apply(rule eq_reflection)
-  apply(rule arg_cong)
-  back
+  apply(rule_tac f="Max" in arg_cong)
   by (auto)
 (*>*)