diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu Sep 15 19:31:17 2016 +0200
+++ b/src/HOL/Library/Library.thy	Thu Sep 15 22:41:05 2016 +0200
@@ -26,6 +26,7 @@
   Extended_Nonnegative_Real
   Extended_Real
   FinFun
+  Finite_Map
   Float
   Formal_Power_Series
   Fraction_Field