src/HOL/Data_Structures/Sorting.thy

--- a/src/HOL/Data_Structures/Sorting.thy	Mon Jan 04 19:56:33 2021 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy	Mon Jan 04 19:41:38 2021 +0100
@@ -272,7 +272,7 @@
 subsubsection "Functional Correctness"
 
 abbreviation mset_mset :: "'a list list \<Rightarrow> 'a multiset" where
-"mset_mset xss \<equiv> \<Union># (image_mset mset (mset xss))"
+"mset_mset xss \<equiv> \<Sum>\<^sub># (image_mset mset (mset xss))"
 
 lemma mset_merge_adj:
   "mset_mset (merge_adj xss) = mset_mset xss"