diff -r 786edc984c98 -r a5c9002bc54d src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -880,7 +880,7 @@
   @{term "{#x+x|x:#M. x<c#}"}.
 *}
 
-enriched_type image_mset: image_mset
+functor image_mset: image_mset
 proof -
   fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
   proof