# HG changeset patch
# User haftmann
# Date 1260391092 -3600
# Node ID f3f0e20923a716836bab9ef3470c1abff64d5ff0
# Parent  97fd820dd4028dd3bc35387d0806cc46623d3e99
take and drop as projections of chop

diff -r 97fd820dd402 -r f3f0e20923a7 src/Pure/library.ML
--- 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 _ [] = ([], [])