tuned

--- a/src/HOL/Data_Structures/Sorting.thy	Sat Nov 07 23:20:43 2020 +0000
+++ b/src/HOL/Data_Structures/Sorting.thy	Sun Nov 08 15:02:50 2020 +0100
@@ -38,7 +38,7 @@
 apply (simp add: mset_insort)
 done
 
-lemma set_insort: "set (insort x xs) = insert x (set xs)"
+lemma set_insort: "set (insort x xs) = {x} \<union> set xs"
 by(simp add: mset_insort flip: set_mset_mset)
 
 lemma sorted_insort: "sorted (insort a xs) = sorted xs"