diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/List.thy --- a/src/HOL/List.thy Tue Dec 21 16:14:46 2010 +0100 +++ b/src/HOL/List.thy Tue Dec 21 17:52:23 2010 +0100 @@ -881,8 +881,8 @@ "length xs = length ys \ map snd (zip xs ys) = ys" by (induct rule:list_induct2, simp_all) -type_lifting map - by simp_all +type_lifting map: map + by (simp_all add: fun_eq_iff id_def) subsubsection {* @{text rev} *}