# HG changeset patch
# User paulson
# Date 1267551376 0
# Node ID 64d2d54cbf03f2491a7389cf38653313d573c268
# Parent  13e83ce8391bb6c06e08f9b6f3cd759963f5dae6
Slightly generalised a theorem

diff -r 13e83ce8391b -r 64d2d54cbf03 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Mar 02 12:59:16 2010 +0000
+++ b/src/HOL/List.thy	Tue Mar 02 17:36:16 2010 +0000
@@ -761,13 +761,13 @@
 by(induct ys, auto simp add: Cons_eq_map_conv)
 
 lemma map_eq_imp_length_eq:
-  assumes "map f xs = map f ys"
+  assumes "map f xs = map g ys"
   shows "length xs = length ys"
 using assms proof (induct ys arbitrary: xs)
   case Nil then show ?case by simp
 next
   case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
-  from Cons xs have "map f zs = map f ys" by simp
+  from Cons xs have "map f zs = map g ys" by simp
   moreover with Cons have "length zs = length ys" by blast
   with xs show ?case by simp
 qed