src/HOL/Nonstandard_Analysis/HSeries.thy

--- a/src/HOL/Nonstandard_Analysis/HSeries.thy	Mon Sep 19 12:53:30 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy	Mon Sep 19 20:06:21 2016 +0200
@@ -59,7 +59,7 @@
 
 lemma sumhr_mult:
   "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
-unfolding sumhr_app by transfer (rule setsum_right_distrib)
+unfolding sumhr_app by transfer (rule setsum_distrib_left)
 
 lemma sumhr_split_add:
   "!!n p. n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"