tuned signature: remove unused;
authorwenzelm
Sun, 05 Dec 2021 16:46:50 +0100
changeset 74883 f32ac01aef5e
parent 74882 947bb3e09a88
child 74884 229d7ea628c2
tuned signature: remove unused;
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