diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -146,6 +146,6 @@
   by (cases m) simp
 
 
-hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
+hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
 
 end
\ No newline at end of file