# HG changeset patch
# User wenzelm
# Date 1638719210 -3600
# Node ID f32ac01aef5ed0836ca43ea52fa728803cf0c33c
# Parent  947bb3e09a885f0aa58ea1f7fb4769eba92bbade
tuned signature: remove unused;

diff -r 947bb3e09a88 -r f32ac01aef5e src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Dec 05 16:26:03 2021 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Dec 05 16:46:50 2021 +0100
@@ -14,7 +14,6 @@
   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