diff -r 8230358fab88 -r feea9cf343d9 src/HOL/Probability/Random_Permutations.thy
--- a/src/HOL/Probability/Random_Permutations.thy	Tue May 24 17:42:14 2016 +0200
+++ b/src/HOL/Probability/Random_Permutations.thy	Tue May 24 18:46:51 2016 +0200
@@ -40,7 +40,7 @@
 text \<open>
   A generic fold function that takes a function, an initial state, and a set 
   and chooses a random order in which it then traverses the set in the same 
-  fashion as a left fold over a list.
+  fashion as a left-fold over a list.
     We first give a recursive definition.
 \<close>
 function fold_random_permutation :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b pmf" where