diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,9 +8,9 @@
 imports
   Euclidean_Space
   L2_Norm
-  "~~/src/HOL/Library/Numeral_Type"
-  "~~/src/HOL/Library/Countable_Set"
-  "~~/src/HOL/Library/FuncSet"
+  "HOL-Library.Numeral_Type"
+  "HOL-Library.Countable_Set"
+  "HOL-Library.FuncSet"
 begin
 
 subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>