diff -r 6ea0e7c43c4f -r e564c3d2d174 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/List.thy	Fri Nov 29 09:48:28 2002 +0100
@@ -431,10 +431,13 @@
 lemma rev_map: "rev (map f xs) = map f (rev xs)"
 by (induct xs) auto
 
+lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
+by (induct xs) auto
+
 lemma map_cong [recdef_cong]:
 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
 -- {* a congruence rule for @{text map} *}
-by (clarify, induct ys) auto
+by simp
 
 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
 by (cases xs) auto