author | haftmann |
Wed, 09 Dec 2009 21:38:12 +0100 | |
changeset 34059 | f3f0e20923a7 |
parent 34058 | 97fd820dd402 |
child 34060 | 69e1dcf20608 |
--- 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 _ [] = ([], [])