diff -r 771117253634 -r 25ca91279a9b src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -712,7 +712,7 @@
 by (simp add: real_of_nat_def del: of_nat_Suc)
 
 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
-by (simp add: real_of_nat_def)
+by (simp add: real_of_nat_def of_nat_mult)
 
 lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
     (SUM x:A. real(f x))"