# HG changeset patch
# User nipkow
# Date 796812239 -7200
# Node ID 95c148a7b9c42505d00ed4a542b7f521c6543c55
# Parent  b5e3fa9664fed5b038cf58f612b7a9fc45206857
generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs)

diff -r b5e3fa9664fe -r 95c148a7b9c4 src/HOL/List.ML
--- 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";