# HG changeset patch
# User haftmann
# Date 1260538357 -3600
# Node ID 5ed4fe8a659d75f4ba9d3b8c6f8e9f629559116f
# Parent  2858dc25eebcf1e9749f3084533eebcf93ef586d# Parent  050bc943d9ba6184ee444f6942aef655ab087692
merged

diff -r 2858dc25eebc -r 5ed4fe8a659d NEWS
--- 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)
diff -r 2858dc25eebc -r 5ed4fe8a659d src/Pure/Isar/rule_cases.ML
--- 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
 
diff -r 2858dc25eebc -r 5ed4fe8a659d src/Pure/library.ML
--- 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 _ [] = ([], [])