changeset 34059 | f3f0e20923a7 |
parent 33955 | fff6f11b1f09 |
child 35976 | ea3d4691a8c6 |
--- a/src/Pure/library.ML Wed Dec 09 21:38:12 2009 +0100 +++ b/src/Pure/library.ML Wed Dec 09 21:38:12 2009 +0100 @@ -425,13 +425,11 @@ fun take (0: int) xs = [] | take _ [] = [] - | take n (x :: xs) = - if n > 0 then x :: take (n - 1) xs else []; + | take n (x :: xs) = x :: take (n - 1) xs; fun drop (0: int) xs = xs | drop _ [] = [] - | drop n (x :: xs) = - if n > 0 then drop (n - 1) xs else x :: xs; + | drop n (x :: xs) = drop (n - 1) xs; fun chop (0: int) xs = ([], xs) | chop _ [] = ([], [])