--- a/src/HOL/Algebra/FiniteProduct.thy Fri Mar 14 12:23:59 2014 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Fri Mar 14 14:29:33 2014 +0100
@@ -456,7 +456,7 @@
text {*Usually, if this rule causes a failed congruence proof error,
the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
Adding @{thm [source] Pi_def} to the simpset is often useful.
- For this reason, @{thm [source] comm_monoid.finprod_cong}
+ For this reason, @{thm [source] finprod_cong}
is not added to the simpset by default.
*}