src/HOL/UNITY/Transformers.thy

--- a/src/HOL/UNITY/Transformers.thy	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/UNITY/Transformers.thy	Sat Mar 22 08:37:43 2014 +0100
@@ -346,7 +346,7 @@
 apply (rule equalityI)
  apply (simp_all add: Un_upper1) 
 apply (simp add: wens_single_def wp_UN_eq, clarify) 
-apply (rule_tac a="Suc(i)" in UN_I, auto) 
+apply (rule_tac a="Suc xa" in UN_I, auto) 
 done
 
 lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}"