diff -r f4b4fba60b1d -r 3b6a3632e754 src/HOL/Probability/Distribution_Functions.thy
--- a/src/HOL/Probability/Distribution_Functions.thy	Fri Sep 30 12:00:17 2016 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy	Fri Sep 30 15:35:32 2016 +0200
@@ -17,7 +17,7 @@
  should be somewhere else. *)
 
 theory Distribution_Functions
-  imports Probability_Measure "~~/src/HOL/Library/Continuum_Not_Denumerable"
+  imports Probability_Measure
 begin
 
 lemma UN_Ioc_eq_UNIV: "(\<Union>n. { -real n <.. real n}) = UNIV"