# HG changeset patch
# User huffman
# Date 1326212065 -3600
# Node ID de2dc5f5277dcbe5059ad3e50a39aabf8e7daa8e
# Parent  5cc700033194c30a42ff66c91c49aa260e99b34f# Parent  19f68d7671f03aafccfee1b75146315ffe95f1f7
merged

diff -r 5cc700033194 -r de2dc5f5277d src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Tue Jan 10 15:43:16 2012 +0100
+++ b/src/HOL/Library/AList.thy	Tue Jan 10 17:14:25 2012 +0100
@@ -173,6 +173,7 @@
 
 hide_const valterm_empty valterm_update random_aux_alist
 
+hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
 hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
 
 end
\ No newline at end of file
diff -r 5cc700033194 -r de2dc5f5277d src/HOL/Library/AList_Impl.thy
--- a/src/HOL/Library/AList_Impl.thy	Tue Jan 10 15:43:16 2012 +0100
+++ b/src/HOL/Library/AList_Impl.thy	Tue Jan 10 17:14:25 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
diff -r 5cc700033194 -r de2dc5f5277d src/HOL/Library/AList_Mapping.thy
--- a/src/HOL/Library/AList_Mapping.thy	Tue Jan 10 15:43:16 2012 +0100
+++ b/src/HOL/Library/AList_Mapping.thy	Tue Jan 10 17:14:25 2012 +0100
@@ -30,11 +30,11 @@
   by (cases xs) (simp_all add: is_empty_def null_def)
 
 lemma update_Mapping [code]:
-  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
+  "Mapping.update k v (Mapping xs) = Mapping (AList_Impl.update k v xs)"
   by (rule mapping_eqI) (simp add: update_conv')
 
 lemma delete_Mapping [code]:
-  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
+  "Mapping.delete k (Mapping xs) = Mapping (AList_Impl.delete k xs)"
   by (rule mapping_eqI) (simp add: delete_conv')
 
 lemma ordered_keys_Mapping [code]: