# HG changeset patch
# User blanchet
# Date 1639755402 -3600
# Node ID 7ada0c20379bd08ed86c33dc4301924eef7f4a31
# Parent  0dd14d8b16da51396b68ce0c7e8336c9f4bdddf7
tuned comment

diff -r 0dd14d8b16da -r 7ada0c20379b src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Dec 17 16:36:42 2021 +0100
@@ -522,7 +522,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