# HG changeset patch
# User blanchet
# Date 1626271797 -7200
# Node ID 291f7b5fc7c9cbfca6c3516f2636eb1df60950fa
# Parent  e5322146e7e81a425d9a162c839683720ad6800b
prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent

diff -r e5322146e7e8 -r 291f7b5fc7c9 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 14 15:18:11 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 14 16:09:57 2021 +0200
@@ -176,10 +176,11 @@
 (* Reject theorems with names like "List.filter.filter_list_def" or "Accessible_Part.acc.defs", as
    these are definitions arising from packages. *)
 fun is_package_def s =
+  exists (fn suf => String.isSuffix suf s)
+    ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
+  andalso
   let val ss = Long_Name.explode s in
-    length ss > 2 andalso not (hd ss = "local") andalso
-    exists (fn suf => String.isSuffix suf s)
-      ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
+    length ss > 2 andalso not (hd ss = "local")
   end
 
 (* FIXME: put other record thms here, or declare as "no_atp" *)
@@ -477,7 +478,8 @@
         else
           let
             val n = length ths
-            val multi = n > 1
+            val collection = n > 1
+            val dotted_name = length (Long_Name.explode name0) > 2 (* ignore theory name *)
 
             fun check_thms a =
               (case try (Proof_Context.get_thms ctxt) a of
@@ -508,21 +510,23 @@
                                  name0
                              end
                          end
-                         |> make_name keywords multi j
+                         |> make_name keywords collection j
                      val stature = stature_of_thm global assms chained css name0 th
                      val new = ((get_name, stature), th)
                    in
-                     (if multi then apsnd else apfst) (cons new) accum
+                     (if collection then apsnd o apsnd
+                      else if dotted_name then apsnd o apfst
+                      else apfst) (cons new) accum
                    end)
               end) ths (n, accum))
           end)
   in
-    (* 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. *)
-    ([], [])
+    (* Names like "xxx" are preferred to "xxx.yyy", which are preferred to "xxx(666)" and the like.
+       "Preferred" means put to the front of  the list. *)
+    ([], ([], []))
     |> add_facts false fold local_facts (unnamed_locals @ named_locals)
     |> add_facts true Facts.fold_static global_facts global_facts
-    |> op @
+    ||> op @ |> op @
   end
 
 fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts