author | wenzelm |
Tue, 09 May 2023 00:41:01 +0200 | |
changeset 77999 | ec850750db87 |
parent 77998 | cad50a7c8091 |
child 78000 | f589c50e54a0 |
--- 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,