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