1.1 --- a/src/HOL/List.thy	Fri Mar 05 12:11:54 1999 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Mar 08 13:49:14 1999 +0100
     1.3 @@ -140,7 +140,7 @@
     1.4    "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
     1.5  primrec
     1.6    "zip xs []     = []"
     1.7 -  "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
     1.8 +  "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
     1.9  primrec
    1.10    "[i..0(] = []"
    1.11    "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"