diff -r 6b480efe1bc3 -r 1d8a79aa2a99 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed Mar 24 21:17:19 2021 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu Mar 25 08:52:15 2021 +0000
@@ -29,17 +29,15 @@
   Euclidean_Algorithm.Lcm
   "Gcd :: _ poly set \<Rightarrow> _"
   "Lcm :: _ poly set \<Rightarrow> _"
-  permutations_of_set
-  permutations_of_multiset
 ]]
 
 text \<open>
   If code generation fails with a message like
   \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>,
-  feel free to add an RBT implementation for the corrsponding operation
-  of delete that code equation (see above).
+  feel free to add an RBT implementation for the corresponding operation
+  or delete that code equation (see above).
 \<close>
- 
+
 export_code _ checking SML OCaml? Haskell? Scala
 
 end