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