| changeset 41505 | 6d19301074cf |
| parent 41372 | 551eb49a6e91 |
| child 43146 | 09f74fda1b1d |
--- a/src/HOL/Library/Dlist.thy Mon Jan 10 22:03:24 2011 +0100 +++ b/src/HOL/Library/Dlist.thy Tue Jan 11 14:12:37 2011 +0100 @@ -175,7 +175,7 @@ section {* Functorial structure *} -type_lifting map: map +enriched_type map: map by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)