--- a/NEWS Fri Dec 11 09:25:45 2009 +0000
+++ b/NEWS Fri Dec 11 14:32:37 2009 +0100
@@ -33,7 +33,7 @@
*** ML ***
-* Curried take and drop. INCOMPATIBILITY.
+* Curried take and drop; negative length is interpreted as infinity. INCOMPATIBILITY.
New in Isabelle2009-1 (December 2009)
--- a/src/Pure/Isar/rule_cases.ML Fri Dec 11 09:25:45 2009 +0000
+++ b/src/Pure/Isar/rule_cases.ML Fri Dec 11 14:32:37 2009 +0100
@@ -144,7 +144,7 @@
(Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
NONE => (name, NONE)
| SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1);
- in fold_rev add_case (drop (n - nprems) cases) ([], n) |> #1 end;
+ in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
in
--- a/src/Pure/library.ML Fri Dec 11 09:25:45 2009 +0000
+++ b/src/Pure/library.ML Fri Dec 11 14:32:37 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 _ [] = ([], [])