src/HOL/Library/Quotient_List.thy
changeset 45802 b16f976db515
parent 40820 fd9c98ead9a9
child 45806 0f1c049c147e
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Fri Dec 09 16:08:32 2011 +0100
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Dec 09 18:07:04 2011 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Main Quotient_Syntax
     1.5  begin
     1.6  
     1.7 -declare [[map list = (map, list_all2)]]
     1.8 +declare [[map list = list_all2]]
     1.9  
    1.10  lemma map_id [id_simps]:
    1.11    "map id = id"