generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs)

--- a/src/HOL/List.ML	Fri Mar 31 15:08:49 1995 +0200
+++ b/src/HOL/List.ML	Sun Apr 02 10:43:59 1995 +0200
@@ -134,7 +134,8 @@
 
 (** Additional mapping lemmas **)
 
-goal List.thy "map (%x.x) xs = xs";
+goal List.thy "map (%x.x) = (%xs.xs)";
+by (rtac ext 1);
 by (list.induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac list_ss));
 qed "map_ident";