--- a/src/HOL/Data_Structures/Sorting.thy Sat Sep 22 16:03:31 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy Sun Sep 23 12:50:12 2018 +0200
@@ -270,7 +270,7 @@
subsubsection "Functional Correctness"
lemma mset_merge_adj:
- "\<Union># image_mset mset (mset (merge_adj xss)) = \<Union># image_mset mset (mset xss)"
+ "\<Union># (image_mset mset (mset (merge_adj xss))) = \<Union># (image_mset mset (mset xss))"
by(induction xss rule: merge_adj.induct) (auto simp: mset_merge)
lemma mset_merge_all: