# HG changeset patch
# User desharna
# Date 1639908921 -3600
# Node ID 6f5eafd952c964abd34d8019757992d57549c425
# Parent  74c53a9027e291d11387a6ce4802eb24b35a9ea3# Parent  7ada0c20379bd08ed86c33dc4301924eef7f4a31
merged

diff -r 74c53a9027e2 -r 6f5eafd952c9 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Dec 18 23:17:08 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -524,7 +524,7 @@
           end)
   in
     (* 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. *)
+       "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