diff -r 1e7c5bbea36d -r 44ce6b524ff3 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Sun Aug 07 12:10:49 2016 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Aug 05 18:34:57 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Infinite Product Measure\<close>
 
 theory Infinite_Product_Measure
-  imports Probability_Measure Caratheodory Projective_Family
+  imports Probability_Measure Projective_Family
 begin
 
 lemma (in product_prob_space) distr_PiM_restrict_finite: