| changeset 41372 | 551eb49a6e91 |
| parent 41229 | d797baa3d57c |
| child 41463 | edbf0a86fb1c |
--- 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 \<Longrightarrow> 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} *}