src/HOL/UNITY/Comp/Priority.thy

--- a/src/HOL/UNITY/Comp/Priority.thy	Wed Jul 02 17:34:45 2014 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy	Wed Jun 11 14:24:23 2014 +1000
@@ -209,7 +209,7 @@
                leadsTo {s. above i s < x}"
 apply (rule leadsTo_UN)
 apply (rule single_leadsTo_I, clarify)
-apply (rule_tac x = "above i x" in above_decreases_lemma)
+apply (rule_tac x = "above i xa" in above_decreases_lemma)
 apply (simp_all (no_asm_use) add: Highest_iff_above0)
 apply blast+
 done