# HG changeset patch
# User haftmann
# Date 1275511550 -7200
# Node ID 812ff0bbd6773762c49ffc01540faf9b41ac6cb6
# Parent  1f3ca94ccb84425fd3cb716b05d13987d8339877# Parent  6315d1bd8388ad3f414f9d9c988355995d528923
merged

diff -r 1f3ca94ccb84 -r 812ff0bbd677 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Wed Jun 02 21:53:03 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Wed Jun 02 22:45:50 2010 +0200
@@ -287,6 +287,7 @@
   by (cases m) simp
 
 
-hide_const (open) 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 default map_entry map_default tabulate bulkload
 
 end
\ No newline at end of file