tuned signature;
authorwenzelm
Tue, 09 May 2023 00:41:01 +0200
changeset 77999 ec850750db87
parent 77998 cad50a7c8091
child 78000 f589c50e54a0
tuned signature;
src/Pure/Syntax/syntax_ext.ML
--- 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,