diff -r da89140186e2 -r c98d1dd7eba1 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Sep 30 15:35:37 2016 +0200
+++ b/src/HOL/Library/Library.thy	Fri Sep 30 15:35:43 2016 +0200
@@ -61,7 +61,7 @@
   Polynomial
   Polynomial_FPS
   Preorder
-  Product_plus
+  Product_Plus
   Quadratic_Discriminant
   Quotient_List
   Quotient_Option