diff -r 1e7c5bbea36d -r 44ce6b524ff3 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Sun Aug 07 12:10:49 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri Aug 05 18:34:57 2016 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Giry_Monad
-  imports Probability_Measure Lebesgue_Integral_Substitution "~~/src/HOL/Library/Monad_Syntax"
+  imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax"
 begin
 
 section \<open>Sub-probability spaces\<close>