src/Pure/Syntax/syntax_ext.ML
changeset 77999 ec850750db87
parent 71545 b0b16088ccf2
child 80748 43c4817375bf
--- a/src/Pure/Syntax/syntax_ext.ML	Mon May 08 23:30:58 2023 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Tue May 09 00:41:01 2023 +0200
@@ -19,7 +19,7 @@
     En
   datatype xprod = XProd of string * xsymb list * string * int
   val chain_pri: int
-  val delims_of: xprod list -> string list list
+  val delims_of: xprod list -> Symbol.symbol list list
   datatype syn_ext =
     Syn_Ext of {
       xprods: xprod list,