src/HOL/Library/Multiset.thy

   but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
   "{#x+x|x:#M. x<c#}"}, where the latter is currently displayed as
   @{term "{#x+x|x:#M. x<c#}"}.
 *}
 
-type_mapper image_mset proof -
+type_lifting image_mset proof -
   fix f g A show "image_mset f (image_mset g A) = image_mset (\<lambda>x. f (g x)) A"
     by (induct A) simp_all
 next
   fix A show "image_mset (\<lambda>x. x) A = A"
     by (induct A) simp_all