--- a/src/Pure/Isar/rule_cases.ML Wed Dec 09 21:33:50 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML Wed Dec 09 21:38:21 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 Wed Dec 09 21:33:50 2009 +0100
+++ b/src/Pure/library.ML Wed Dec 09 21:38:21 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 _ [] = ([], [])