# HG changeset patch
# User wenzelm
# Date 1208425200 -7200
# Node ID 6c7e4d858bae3d0331ed8754ef872c9bbc361df4
# Parent  ca558202ffa5bccd1d3df996dc7cd3b67eaadd0e
unused_thms: sort_distinct;

diff -r ca558202ffa5 -r 6c7e4d858bae src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Wed Apr 16 22:17:43 2008 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Thu Apr 17 11:40:00 2008 +0200
@@ -83,7 +83,9 @@
     fun add_fact (name, ths) =
       if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
       else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
-    val thms = sort_wrt #1 (fold (Facts.fold_static add_fact o PureThy.facts_of) thys []);
+    val thms =
+      fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
+      |> sort_distinct (string_ord o pairself #1);
     val tab = fold Proofterm.thms_of_proof
       (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty;
     fun is_unused (name, th) = case Symtab.lookup tab name of