src/HOL/Library/Quotient_List.thy
changeset 46663 7fe029e818c2
parent 45806 0f1c049c147e
child 47094 1a7ad2601cb5
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Fri Feb 24 18:46:01 2012 +0100
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Feb 24 22:46:16 2012 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  lemma map_id [id_simps]:
     1.6    "map id = id"
     1.7 -  by (fact map.id)
     1.8 +  by (fact List.map.id)
     1.9  
    1.10  lemma list_all2_eq [id_simps]:
    1.11    "list_all2 (op =) = (op =)"