author | haftmann |
Mon, 14 Dec 2009 16:35:00 +0100 | |
changeset 34088 | d6194ece49df |
parent 34087 | c907edcaab36 |
child 34090 | 7f7297f348fe |
--- a/src/Pure/Tools/find_theorems.ML Mon Dec 14 11:30:13 2009 +0000 +++ b/src/Pure/Tools/find_theorems.ML Mon Dec 14 16:35:00 2009 +0100 @@ -409,7 +409,7 @@ val len = length matches; val lim = the_default (! limit) opt_limit; - in (SOME len, drop (len - lim) matches) end; + in (SOME len, drop (Int.max (len - lim, 0)) matches) end; val find = if rem_dups orelse is_none opt_limit