explicit lower bound for index
authorhaftmann
Wed, 09 Dec 2009 21:38:12 +0100
changeset 34058 97fd820dd402
parent 34042 b174d384293e
child 34059 f3f0e20923a7
explicit lower bound for index
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