# HG changeset patch
# User haftmann
# Date 1260391092 -3600
# Node ID 97fd820dd4028dd3bc35387d0806cc46623d3e99
# Parent  b174d384293e9b77855a815b8cf7c022fb512be2
explicit lower bound for index

diff -r b174d384293e -r 97fd820dd402 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Dec 09 12:26:42 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Wed Dec 09 21:38:12 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