src/HOL/Probability/Discrete_Topology.thy

--- a/src/HOL/Probability/Discrete_Topology.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory Discrete_Topology
-imports Multivariate_Analysis
+imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
 begin
 
 text {* Copy of discrete types with discrete topology. This space is polish. *}