# HG changeset patch
# User wenzelm
# Date 1666636652 -7200
# Node ID 1ac2416e843293bc6917ba965f54b42962514b7f
# Parent  9bd948666e8ab57b995a1da72912eba6b6b8ee5a
tuned signature (again, amending f32ac01aef5e), e.g. relevant for Isabelle/DOF;

diff -r 9bd948666e8a -r 1ac2416e8432 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Oct 24 20:24:34 2022 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Oct 24 20:37:32 2022 +0200
@@ -14,6 +14,7 @@
   val macro0: string -> text
   val macro: string -> text -> text
   val environment: string -> text -> text
+  val output_name: string -> string
   val output_ascii: string -> string
   val output_ascii_breakable: string -> string -> string
   val output_symbols: Symbol.symbol list -> string