1.1 --- a/src/HOL/Quotient_Examples/DList.thy	Wed Aug 17 15:12:34 2011 -0700
     1.2 +++ b/src/HOL/Quotient_Examples/DList.thy	Thu Aug 18 16:52:19 2011 +0900
     1.3 @@ -48,6 +48,14 @@
     1.4    by (induct xa ya arbitrary: fx fy rule: list_induct2')
     1.5       (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+
     1.6  
     1.7 +lemma remdups_eq_member_eq:
     1.8 +  assumes "remdups xa = remdups ya"
     1.9 +    shows "List.member xa = List.member ya"
    1.10 +  using assms
    1.11 +  unfolding fun_eq_iff List.member_def
    1.12 +  by (induct xa ya rule: list_induct2')
    1.13 +     (metis remdups_nil_noteq_cons set_remdups)+
    1.14 +
    1.15  text {* Setting up the quotient type *}
    1.16  
    1.17  definition
    1.18 @@ -91,7 +99,7 @@
    1.19    "(op = ===> dlist_eq ===> dlist_eq) map map"
    1.20    "(op = ===> dlist_eq ===> dlist_eq) filter filter"
    1.21    by (auto intro!: fun_relI simp add: remdups_filter)
    1.22 -     (metis (full_types) member_set set_remdups remdups_eq_map_eq)+
    1.23 +     (metis (full_types) set_remdups remdups_eq_map_eq remdups_eq_member_eq)+
    1.24  
    1.25  quotient_definition empty where "empty :: 'a dlist"
    1.26    is "Nil"