# HG changeset patch
# User eberlm
# Date 1464108481 -7200
# Node ID aa573306a9cdfd067d93f685b71c2c9ec4c1a8b4
# Parent  feea9cf343d99a035b5c773a5691e715ca0e8676
Removed problematic code equation for set_permutations

diff -r feea9cf343d9 -r aa573306a9cd src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Tue May 24 18:46:51 2016 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Tue May 24 18:48:01 2016 +0200
@@ -73,6 +73,9 @@
 lemma [code, code del]:
   "Lcm_eucl = Lcm_eucl" ..
 
+lemma [code, code del]:
+  "permutations_of_set = permutations_of_set" ..
+
 (*
   If the code generation ends with an exception with the following message:
   '"List.set" is not a constructor, on left hand side of equation: ...',
diff -r feea9cf343d9 -r aa573306a9cd src/HOL/Probability/Random_Permutations.thy
--- a/src/HOL/Probability/Random_Permutations.thy	Tue May 24 18:46:51 2016 +0200
+++ b/src/HOL/Probability/Random_Permutations.thy	Tue May 24 18:48:01 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