src/Pure/Syntax/syntax_ext.ML

--- a/src/Pure/Syntax/syntax_ext.ML	Thu Dec 12 22:53:06 2024 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Dec 13 23:23:07 2024 +0100
@@ -19,8 +19,8 @@
     Brk of int |
     En
   datatype xprod = XProd of string * xsymb list * string * int
+  val fold_delims: (string -> 'a -> 'a) -> xprod -> 'a -> 'a
   val chain_pri: int
-  val delims_of: xprod list -> Symbol.symbol list list
   datatype syn_ext =
     Syn_Ext of {
       xprods: xprod list,
@@ -107,12 +107,9 @@
 
 datatype xprod = XProd of string * xsymb list * string * int;
 
-val chain_pri = ~1;   (*dummy for chain productions*)
+fun fold_delims f (XProd (_, xsymbs, _, _)) = fold (fn Delim s => f s | _ => I) xsymbs;
 
-fun delims_of xprods =
-  fold (fn XProd (_, xsymbs, _, _) =>
-    fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
-  |> map Symbol.explode;
+val chain_pri = ~1;   (*dummy for chain productions*)