author | haftmann |
Wed, 09 Dec 2009 21:38:12 +0100 | |
changeset 34058 | 97fd820dd402 |
parent 34042 | b174d384293e |
child 34059 | f3f0e20923a7 |
--- 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