diff -r 6a5faa5bcf19 -r 17223cf843d8 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy Thu Mar 27 19:04:38 2008 +0100
+++ b/src/HOL/Library/List_Prefix.thy Thu Mar 27 19:04:39 2008 +0100
@@ -355,15 +355,15 @@
shows "xs \ ys"
using len neq
proof (induct rule: list_induct2)
- case 1
+ case Nil
then show ?case by simp
next
- case (2 a as b bs)
+ case (Cons a as b bs)
have ih: "as \ bs \ as \ bs" by fact
show ?case
proof (cases "a = b")
case True
- then have "as \ bs" using 2 by simp
+ then have "as \ bs" using Cons by simp
then show ?thesis by (rule Cons_parallelI2 [OF True ih])
next
case False