Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/thm_deps.ML
changeset 26699 6c7e4d858bae
parent 26697 3b9eede40608
child 27865 27a8ad9612a3 
--- 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
isabelle