diff -r c686f9abc99c -r 7c58324cd418 src/HOL/Hyperreal/Ln.thy
--- a/src/HOL/Hyperreal/Ln.thy	Thu Jul 03 20:15:06 2008 +0200
+++ b/src/HOL/Hyperreal/Ln.thy	Thu Jul 03 20:53:44 2008 +0200
@@ -85,7 +85,7 @@
       apply (rule mult_nonneg_nonneg)
       apply simp
       apply (subst inverse_nonnegative_iff_nonnegative)
-      apply (rule real_of_nat_fact_ge_zero)
+      apply (rule real_of_nat_ge_zero)
       apply (rule zero_le_power)
       apply (rule a)
       done