diff -r 3b6a3632e754 -r da89140186e2 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Sep 30 15:35:32 2016 +0200
+++ b/src/HOL/Library/Library.thy	Fri Sep 30 15:35:37 2016 +0200
@@ -37,7 +37,6 @@
   Groups_Big_Fun
   Indicator_Function
   Infinite_Set
-  Inner_Product
   IArray
   Lattice_Algebras
   Lattice_Syntax
@@ -62,7 +61,7 @@
   Polynomial
   Polynomial_FPS
   Preorder
-  Product_Vector
+  Product_plus
   Quadratic_Discriminant
   Quotient_List
   Quotient_Option