diff -r 8eb6365f5916 -r b9a1486e79be src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Oct 16 22:43:51 2016 +0200
+++ b/src/HOL/Rat.thy	Mon Oct 17 11:46:22 2016 +0200
@@ -698,7 +698,7 @@
 lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
   by transfer (simp add: divide_inverse nonzero_inverse_mult_distrib ac_simps)
 
-lemma of_rat_setsum: "of_rat (\<Sum>a\<in>A. f a) = (\<Sum>a\<in>A. of_rat (f a))"
+lemma of_rat_sum: "of_rat (\<Sum>a\<in>A. f a) = (\<Sum>a\<in>A. of_rat (f a))"
   by (induct rule: infinite_finite_induct) (auto simp: of_rat_add)
 
 lemma of_rat_setprod: "of_rat (\<Prod>a\<in>A. f a) = (\<Prod>a\<in>A. of_rat (f a))"