prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)

--- a/src/Pure/Isar/find_theorems.ML	Tue Feb 20 00:53:18 2007 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Wed Feb 21 02:30:06 2007 +0100
@@ -280,7 +280,9 @@
     val filters = map (filter_criterion ctxt opt_goal) criteria;
 
     val raw_matches = all_filters filters (find_thms ctxt ([], []));
-    val matches = if rem_dups then rem_thm_dups raw_matches else raw_matches;
+    val matches = if rem_dups andalso not (null filters) 
+                  then rem_thm_dups raw_matches 
+                  else raw_matches;
 
     val len = length matches;
     val limit = the_default (! thms_containing_limit) opt_limit;