# HG changeset patch
# User haftmann
# Date 1260517636 -3600
# Node ID 2231c06ca9e0d7734ee48dd036232aab8b8db975
# Parent  53a8f294d60f246aa10437841f572ebfcdc32c74# Parent  69e1dcf206080338707fa827ad1ff9989bd566b4
merged

diff -r 53a8f294d60f -r 2231c06ca9e0 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Dec 10 22:28:55 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Fri Dec 11 08:47:16 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 53a8f294d60f -r 2231c06ca9e0 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Dec 10 22:28:55 2009 +0100
+++ b/src/Pure/library.ML	Fri Dec 11 08:47:16 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 _ [] = ([], [])