src/HOL/Library/Dlist.thy

--- a/src/HOL/Library/Dlist.thy	Thu Nov 18 17:01:15 2010 +0100
+++ b/src/HOL/Library/Dlist.thy	Thu Nov 18 17:01:15 2010 +0100
@@ -173,6 +173,12 @@
 qed
 
 
+section {* Functorial structure *}
+
+type_mapper map
+  by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
+
+
 section {* Implementation of sets by distinct lists -- canonical! *}
 
 definition Set :: "'a dlist \<Rightarrow> 'a fset" where