*** empty log message ***

--- 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)