# HG changeset patch
# User wenzelm
# Date 1726564465 -7200
# Node ID 3e0ca6af67383aa898b87fbc06dabd1ad33a2cfe
# Parent  68a3defc73d06c2a7429139bb9d0909c8d48b64c
unused (see 39261908e12f);

diff -r 68a3defc73d0 -r 3e0ca6af6738 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Tue Sep 17 11:06:11 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Tue Sep 17 11:14:25 2024 +0200
@@ -7,7 +7,6 @@
 signature SYNTAX_EXT =
 sig
   datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
-  val typ_to_nonterm: typ -> string
   type block = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int}
   val block_indent: int -> block
   datatype xsymb =