# HG changeset patch
# User kleing
# Date 1173154193 -3600
# Node ID 3f189ea9bfe76a64845108db3fb8da08902952e2
# Parent  3df5c44482e20c250b65969d2e7d98fcb07c4a43
an O(n log n) version of removing duplicates

diff -r 3df5c44482e2 -r 3f189ea9bfe7 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Mon Mar 05 22:39:59 2007 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Tue Mar 06 05:09:53 2007 +0100
@@ -233,7 +233,7 @@
 end;
 
 
-(* removing duplicates, preferring nicer names *)
+(* removing duplicates, preferring nicer names, roughly n log n *)
 
 fun rem_thm_dups xs =
   let
@@ -245,21 +245,24 @@
       | nicer (NameSelection (x, _)) (NameSelection (y, _)) = size x <= size y
       | nicer (NameSelection _) _ = false;
 
-    fun is_in [] _ = NONE
-      | is_in ((n, t) :: xs) t' =
-          if Thm.eq_thm (t, t') then SOME (n, t) else is_in xs t';
-
-    fun eq ((_, t1), (_, t2)) = Thm.eq_thm (t1, t2);
+    fun rem_cdups xs =
+      let
+        fun rem_c rev_seen [] = rev rev_seen
+          | rem_c rev_seen [x] = rem_c (x::rev_seen) []
+          | rem_c rev_seen ((x as ((n,t),_))::(y as ((n',t'),_))::xs) =
+            if Thm.eq_thm_prop (t,t')
+            then if nicer n n'
+                 then rem_c rev_seen (x::xs)
+                 else rem_c rev_seen (y::xs)
+            else rem_c (x::rev_seen) (y::xs)
+      in rem_c [] xs end;
 
-    fun rem_d (rev_seen, []) = rev rev_seen
-      | rem_d (rev_seen, (x as (n', t')) :: xs) =
-          (case is_in rev_seen t' of
-            NONE => rem_d (x :: rev_seen, xs)
-          | SOME (n, t) =>
-              if nicer n n'
-              then rem_d (rev_seen, xs)
-              else rem_d (x :: remove eq (n, t) rev_seen, xs))
-  in rem_d ([], xs) end;
+  in ListPair.zip (xs, 1 upto length xs)
+     |> sort (Term.fast_term_ord o pairself (prop_of o #2 o #1))
+     |> rem_cdups
+     |> sort (int_ord o pairself #2)
+     |> map #1
+  end;
 
 
 (* print_theorems *)
@@ -279,7 +282,7 @@
 
     val raw_matches = all_filters filters (find_thms ctxt ([], []));
     val matches =
-      if rem_dups andalso not (null filters)
+      if rem_dups
       then rem_thm_dups raw_matches
       else raw_matches;