# HG changeset patch
# User boehmes
# Date 1260822508 -3600
# Node ID 7f7297f348fe555f840fbe606c40e0c74b9b3387
# Parent  a67bebd37135dbacec97df9b95f6a28be4cb2588# Parent  d6194ece49df94024b792f99821a1b41653977a6
merged

diff -r a67bebd37135 -r 7f7297f348fe src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Dec 14 21:27:59 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Dec 14 21:28:28 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