src/HOL/Transcendental.thy

--- a/src/HOL/Transcendental.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Transcendental.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -971,7 +971,7 @@
 
 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
 unfolding exp_def
-apply (subst of_real.suminf)
+apply (subst suminf_of_real)
 apply (rule summable_exp_generic)
 apply (simp add: scaleR_conv_of_real)
 done