--- a/src/HOL/Library/Mapping.thy Mon Dec 23 16:59:56 2013 +0100
+++ b/src/HOL/Library/Mapping.thy Mon Dec 23 16:29:43 2013 +0100
@@ -142,11 +142,11 @@
definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
"map_default k v f m = map_entry k f (default k v m)"
-lift_definition assoc_list_to_mapping :: "('k \<times> 'v) list \<Rightarrow> ('k, 'v) mapping"
+lift_definition of_alist :: "('k \<times> 'v) list \<Rightarrow> ('k, 'v) mapping"
is map_of parametric map_of_transfer .
-lemma assoc_list_to_mapping_code [code]:
- "assoc_list_to_mapping xs = foldr (\<lambda>(k, v) m. update k v m) xs empty"
+lemma of_alist_code [code]:
+ "of_alist xs = foldr (\<lambda>(k, v) m. update k v m) xs empty"
by transfer(simp add: map_add_map_of_foldr[symmetric])
instantiation mapping :: (type, type) equal
@@ -364,7 +364,7 @@
code_datatype empty update
hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size
- replace default map_entry map_default tabulate bulkload map
+ replace default map_entry map_default tabulate bulkload map of_alist
end