diff -r 1b2e882f42d2 -r 19f68d7671f0 src/HOL/Library/AList_Impl.thy
--- a/src/HOL/Library/AList_Impl.thy	Tue Jan 10 10:48:39 2012 +0100
+++ b/src/HOL/Library/AList_Impl.thy	Tue Jan 10 15:48:10 2012 +0100
@@ -693,6 +693,6 @@
   shows "distinct (map fst (map_default k v f xs))"
 using assms by (induct xs) (auto simp add: dom_map_default)
 
-hide_const (open) map_entry
+hide_const (open) update updates delete restrict clearjunk merge compose map_entry
 
 end