--- a/src/HOL/Library/Dlist.thy Sun Dec 05 14:02:16 2010 +0100
+++ b/src/HOL/Library/Dlist.thy Mon Dec 06 09:19:10 2010 +0100
@@ -175,7 +175,7 @@
section {* Functorial structure *}
-type_mapper map
+type_lifting map
by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)