# HG changeset patch
# User kleing
# Date 1172021406 -3600
# Node ID 8e0f61d05f48c5abf9d5ba2ce62dd23962f93647
# Parent  0b990dc39ea2fa290041ee3e0395babed9477452
prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)

diff -r 0b990dc39ea2 -r 8e0f61d05f48 src/Pure/Isar/find_theorems.ML
--- 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;