src/Pure/Tools/find_theorems.ML

           then rem_thm_dups (nicer_shortest ctxt) raw_matches
           else raw_matches;
 
         val len = length matches;
         val lim = the_default (! limit) opt_limit;
-      in (SOME len, (uncurry drop) (len - lim, matches)) end;
+      in (SOME len, drop (len - lim) matches) end;
 
     val find =
       if rem_dups orelse is_none opt_limit
       then find_all
       else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;