unused (see 39261908e12f);
authorwenzelm
Tue, 17 Sep 2024 11:14:25 +0200
changeset 80894 3e0ca6af6738
parent 80893 68a3defc73d0
child 80895 2870315eea9e
unused (see 39261908e12f);
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 =