diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -1001,7 +1001,7 @@
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)
 
-hide (open) const bagify
+hide_const (open) bagify
 
 
 subsection {* The multiset order *}