diff -r ab0234b9af65 -r af34fcf7215d src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Sep 11 21:41:33 2024 +0200
+++ b/src/Pure/General/pretty.ML	Wed Sep 11 22:28:42 2024 +0200
@@ -77,6 +77,7 @@
   val output: output_ops -> T -> Bytes.T
   val string_of_ops: output_ops -> T -> string
   val string_of: T -> string
+  val pure_string_of: T -> string
   val writeln: T -> unit
   val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T
@@ -428,6 +429,8 @@
 fun string_of_ops ops = Bytes.content o output ops;
 fun string_of prt = string_of_ops (output_ops NONE) prt;
 
+val pure_string_of = string_of_ops (pure_output_ops NONE);
+
 fun writeln prt =
   Output.writelns (Bytes.contents (output (output_ops NONE) prt));