diff -r b6a1047bc164 -r 9d4dbb7a548a src/HOL/Probability/Distribution_Functions.thy
--- a/src/HOL/Probability/Distribution_Functions.thy	Tue Jul 12 16:04:19 2016 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy	Tue Jul 12 19:12:17 2016 +0200
@@ -17,7 +17,7 @@
  should be somewhere else. *)
 
 theory Distribution_Functions
-  imports Probability_Measure "~~/src/HOL/Library/ContNotDenum"
+  imports Probability_Measure "~~/src/HOL/Library/Continuum_Not_Denumerable"
 begin
 
 lemma UN_Ioc_eq_UNIV: "(\<Union>n. { -real n <.. real n}) = UNIV"