# HG changeset patch
# User nipkow
# Date 1073338983 -3600
# Node ID a1add2de7601b24c3f4f8eb9e5807fb135d1cb4c
# Parent  e13731554e50626b07571b2c3692a0292ef37d70
*** empty log message ***

diff -r e13731554e50 -r a1add2de7601 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jan 05 00:46:06 2004 +0100
+++ b/src/HOL/List.thy	Mon Jan 05 22:43:03 2004 +0100
@@ -488,8 +488,8 @@
 by(induct ys, auto)
 
 lemma map_injective:
- "!!xs. map f xs = map f ys ==> (\<forall>x y. f x = f y --> x = y) ==> xs = ys"
-by (induct ys) auto
+ "!!xs. map f xs = map f ys ==> inj f ==> xs = ys"
+by (induct ys) (auto dest!:injD)
 
 lemma inj_mapI: "inj f ==> inj (map f)"
 by (rules dest: map_injective injD intro: inj_onI)