src/HOL/Library/AList_Impl.thy
changeset 46171 19f68d7671f0
parent 46133 d9fe85d3d2cd
--- 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