--- 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