1.1 --- a/src/HOL/Library/Quotient_List.thy	Thu Apr 26 01:05:06 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Thu Apr 26 12:01:58 2012 +0200
     1.3 @@ -178,7 +178,7 @@
     1.4  
     1.5  subsection {* Setup for lifting package *}
     1.6  
     1.7 -lemma Quotient_list:
     1.8 +lemma Quotient_list[quot_map]:
     1.9    assumes "Quotient R Abs Rep T"
    1.10    shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"
    1.11  proof (unfold Quotient_alt_def, intro conjI allI impI)
    1.12 @@ -199,8 +199,6 @@
    1.13      by (induct xs ys rule: list_induct2', simp_all, metis 3)
    1.14  qed
    1.15  
    1.16 -declare [[map list = (list_all2, Quotient_list)]]
    1.17 -
    1.18  lemma list_invariant_commute [invariant_commute]:
    1.19    "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
    1.20    apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def)