diff -r 80c361e9d19d -r dd651e3f7413 src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Mon May 23 22:43:22 2016 +0200
+++ b/src/HOL/Probability/Probability.thy	Tue May 24 15:05:41 2016 +0200
@@ -9,6 +9,7 @@
   Projective_Limit
   Probability_Mass_Function
   Stream_Space
+  Random_Permutations
   Embed_Measure
   Central_Limit_Theorem
 begin