src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 80820 db114ec720cb
parent 80636 4041e7c8059d
child 80874 9af593e9e454
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -318,7 +318,7 @@
 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
 
 fun quot_normal_name_for_type ctxt T =
-  quot_normal_prefix ^ YXML.content_of (Syntax.string_of_typ ctxt T)
+  quot_normal_prefix ^ Protocol_Message.clean_output (Syntax.string_of_typ ctxt T)
 
 val strip_first_name_sep =
   Substring.full #> Substring.position name_sep ##> Substring.triml 1