--- a/src/HOL/List.thy Sun Dec 05 14:02:16 2010 +0100
+++ b/src/HOL/List.thy Mon Dec 06 09:19:10 2010 +0100
@@ -881,7 +881,7 @@
"length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
by (induct rule:list_induct2, simp_all)
-type_mapper map
+type_lifting map
by simp_all