# HG changeset patch
# User bulwahn
# Date 1323935474 -3600
# Node ID 58a10da12812f2e11dad30718b026f4f2b3470b9
# Parent  cf7ef3fca5e484e29ae151e0dc964a23af3a8047
hiding the precious name map_entry in AList_Impl

diff -r cf7ef3fca5e4 -r 58a10da12812 src/HOL/Library/AList_Impl.thy
--- a/src/HOL/Library/AList_Impl.thy	Wed Dec 14 23:08:03 2011 +0100
+++ b/src/HOL/Library/AList_Impl.thy	Thu Dec 15 08:51:14 2011 +0100
@@ -693,4 +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
+
 end