--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Sep 06 20:31:20 2024 +0200
@@ -162,7 +162,7 @@
fun nth_name j =
(case xref of
- Facts.Fact s => cartouche (simplify_spaces (YXML.content_of s)) ^ bracket
+ Facts.Fact s => cartouche (simplify_spaces (Protocol_Message.clean_output s)) ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
| Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
| Facts.Named ((name, _), SOME intervals) =>