diff -r be149db8207a -r 96b56c98f346 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Fri Nov 04 15:22:12 2016 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Nov 04 18:18:30 2016 +0100
@@ -5,7 +5,7 @@
 section \<open>Finite Maps\<close>
 
 theory Fin_Map
-  imports Finite_Product_Measure "~~/src/HOL/Library/Finite_Map"
+  imports "~~/src/HOL/Analysis/Finite_Product_Measure" "~~/src/HOL/Library/Finite_Map"
 begin
 
 text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of