diff -r 994a2b9daf1d -r 8f7f626aacaa src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Oct 30 11:59:23 2021 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Oct 30 11:59:41 2021 +0200
@@ -3307,15 +3307,11 @@
 
 setup \<open>
   let
-    fun msetT T = Type (\<^type_name>\<open>multiset\<close>, [T]);
-
-    fun mk_mset T [] = Const (\<^const_abbrev>\<open>empty_mset\<close>, msetT T)
-      | mk_mset T [x] =
-        Const (\<^const_name>\<open>add_mset\<close>, T --> msetT T --> msetT T) $ x $
-          Const (\<^const_abbrev>\<open>empty_mset\<close>, msetT T)
-      | mk_mset T (x :: xs) =
-        Const (\<^const_name>\<open>plus\<close>, msetT T --> msetT T --> msetT T) $
-          mk_mset T [x] $ mk_mset T xs
+    fun msetT T = \<^Type>\<open>multiset T\<close>;
+
+    fun mk_mset T [] = \<^instantiate>\<open>'a = T in term \<open>{#}\<close>\<close>
+      | mk_mset T [x] = \<^instantiate>\<open>'a = T and x in term \<open>{#x#}\<close>\<close>
+      | mk_mset T (x :: xs) = \<^Const>\<open>plus \<open>msetT T\<close> for \<open>mk_mset T [x]\<close> \<open>mk_mset T xs\<close>\<close>
 
     fun mset_member_tac ctxt m i =
       if m <= 0 then
@@ -3420,10 +3416,8 @@
           in
             (case maps elems_for (all_values elem_T) @
                  (if maybe_opt then [Const (Nitpick_Model.unrep_mixfix (), elem_T)] else []) of
-              [] => Const (\<^const_name>\<open>zero_class.zero\<close>, T)
-            | ts =>
-                foldl1 (fn (s, t) => Const (\<^const_name>\<open>add_mset\<close>, elem_T --> T --> T) $ s $ t)
-                  ts)
+              [] => \<^Const>\<open>Groups.zero T\<close>
+            | ts => foldl1 (fn (s, t) => \<^Const>\<open>add_mset elem_T for s t\<close>) ts)
           end
       | multiset_postproc _ _ _ _ t = t
   in Nitpick_Model.register_term_postprocessor \<^typ>\<open>'a multiset\<close> multiset_postproc end