src/HOL/List.ML
changeset 14025 d9b155757dc8
parent 13122 c63612ffb186
child 14401 477380c74c1d
     1.1 --- a/src/HOL/List.ML	Tue May 13 08:59:21 2003 +0200
     1.2 +++ b/src/HOL/List.ML	Wed May 14 10:22:09 2003 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4  val map_compose = thm "map_compose";
     1.5  val map_concat = thm "map_concat";
     1.6  val map_cong = thm "map_cong";
     1.7 -val map_eq_Cons = thm "map_eq_Cons";
     1.8 +val map_eq_Cons_conv = thm "map_eq_Cons_conv";
     1.9  val map_ext = thm "map_ext";
    1.10  val map_ident = thm "map_ident";
    1.11  val map_injective = thm "map_injective";