diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri May 13 20:24:10 2016 +0200
@@ -771,7 +771,7 @@
     done
   with M show "subprob_space (join M)"
     by (intro subprob_spaceI)
-       (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
+       (auto simp: emeasure_join space_subprob_algebra M dest: subprob_space.emeasure_space_le_1)
 next
   assume "\<not>(space N \<noteq> {})"
   thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)