diff -r 4874411752fe -r 7edb7550663e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Transcendental.thy	Fri May 30 14:55:10 2014 +0200
@@ -76,10 +76,7 @@
 lemma lemma_realpow_rev_sumr:
    "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
     (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
-  apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
-  apply (auto simp: image_iff Bex_def intro!: inj_onI)
-  apply arith
-  done
+  by (subst nat_diff_setsum_reindex[symmetric]) simp
 
 lemma power_diff_1_eq:
   fixes x :: "'a::{comm_ring,monoid_mult}"