
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 \<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} *}




