# HG changeset patch
# User wenzelm
# Date 1394803773 -3600
# Node ID 8bb21318e10b184440cf8fe0266298c29b0780d7
# Parent  c06202417c4a207f36609b0a22c66a1ce38f32f7
tuned -- command 'text' was localized some years ago;

diff -r c06202417c4a -r 8bb21318e10b src/HOL/Algebra/FiniteProduct.thy
--- 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.
 *}