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,