# HG changeset patch
# User blanchet
# Date 1357490309 -3600
# Node ID c96bb430ddb02554087c050b0a172b72527ba719
# Parent  4c781d65c0d616f30c11313b0792170e15bc8351
put single-theorem names before multi-theorem ones (broken since 5d147d492792)

diff -r 4c781d65c0d6 -r c96bb430ddb0 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Jan 06 17:38:29 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Jan 06 17:38:29 2013 +0100
@@ -453,13 +453,13 @@
               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
           in
             pair n
-            #> fold_rev (fn th => fn (j, (multis, unis)) =>
+            #> fold_rev (fn th => fn (j, accum) =>
                    (j - 1,
                     if not (member Thm.eq_thm_prop add_ths th) andalso
                        (is_likely_tautology_too_meta_or_too_technical th orelse
                         (not generous andalso
                          is_too_complex ho_atp (prop_of th))) then
-                      (multis, unis)
+                      accum
                     else
                       let
                         val new =
@@ -469,23 +469,24 @@
                                 else
                                   [Facts.extern ctxt facts name0,
                                    Name_Space.extern ctxt full_space name0]
+                                  |> distinct (op =)
                                   |> find_first check_thms
                                   |> the_default name0
                                   |> make_name reserved multi j),
                              stature_of_thm global assms chained css name0 th),
                            th)
                       in
-                        if multi then (new :: multis, unis)
-                        else (multis, new :: unis)
+                        accum |> (if multi then apsnd else apfst) (cons new)
                       end)) ths
             #> snd
           end)
   in
-    (* The single-name theorems go after the multiple-name ones, so that single
-       names are preferred when both are available. *)
-    ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
-             |> add_facts true Facts.fold_static global_facts global_facts
-             |> op @
+    (* The single-theorem names go before the multiple-theorem ones (e.g.,
+       "xxx" vs. "xxx(3)"), so that single names are preferred when both are
+       available. *)
+    `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
+          |> add_facts true Facts.fold_static global_facts global_facts
+          |> op @
   end
 
 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts