1.1 --- a/src/HOL/Library/AList.thy	Tue Jan 10 10:48:39 2012 +0100
     1.2 +++ b/src/HOL/Library/AList.thy	Tue Jan 10 15:48:10 2012 +0100
     1.3 @@ -173,6 +173,7 @@
     1.4  
     1.5  hide_const valterm_empty valterm_update random_aux_alist
     1.6  
     1.7 +hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
     1.8  hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
     1.9  
    1.10  end
    1.11 \ No newline at end of file

     2.1 --- a/src/HOL/Library/AList_Impl.thy	Tue Jan 10 10:48:39 2012 +0100
     2.2 +++ b/src/HOL/Library/AList_Impl.thy	Tue Jan 10 15:48:10 2012 +0100
     2.3 @@ -693,6 +693,6 @@
     2.4    shows "distinct (map fst (map_default k v f xs))"
     2.5  using assms by (induct xs) (auto simp add: dom_map_default)
     2.6  
     2.7 -hide_const (open) map_entry
     2.8 +hide_const (open) update updates delete restrict clearjunk merge compose map_entry
     2.9  
    2.10  end

     3.1 --- a/src/HOL/Library/AList_Mapping.thy	Tue Jan 10 10:48:39 2012 +0100
     3.2 +++ b/src/HOL/Library/AList_Mapping.thy	Tue Jan 10 15:48:10 2012 +0100
     3.3 @@ -30,11 +30,11 @@
     3.4    by (cases xs) (simp_all add: is_empty_def null_def)
     3.5  
     3.6  lemma update_Mapping [code]:
     3.7 -  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
     3.8 +  "Mapping.update k v (Mapping xs) = Mapping (AList_Impl.update k v xs)"
     3.9    by (rule mapping_eqI) (simp add: update_conv')
    3.10  
    3.11  lemma delete_Mapping [code]:
    3.12 -  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
    3.13 +  "Mapping.delete k (Mapping xs) = Mapping (AList_Impl.delete k xs)"
    3.14    by (rule mapping_eqI) (simp add: delete_conv')
    3.15  
    3.16  lemma ordered_keys_Mapping [code]: