# HG changeset patch
# User haftmann
# Date 1260804900 -3600
# Node ID d6194ece49df94024b792f99821a1b41653977a6
# Parent  c907edcaab36ced3bfedd3305cfadda4bb0c0a7e
avoid negative indices as argument ot drop

diff -r c907edcaab36 -r d6194ece49df src/Pure/Tools/find_theorems.ML
--- 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