diff -r 68dc8ffc94c2 -r 81a72b7fcb0c src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Thu Dec 12 22:53:06 2024 +0100
+++ b/src/Pure/General/scan.ML	Fri Dec 13 23:23:07 2024 +0100
@@ -87,6 +87,7 @@
   val is_literal: lexicon -> string list -> bool
   val literal: lexicon -> (string * 'a) list -> (string * 'a) list * (string * 'a) list
   val empty_lexicon: lexicon
+  val build_lexicon: (lexicon -> lexicon) -> lexicon
   val extend_lexicon: string list -> lexicon -> lexicon
   val make_lexicon: string list list -> lexicon
   val dest_lexicon: lexicon -> string list
@@ -308,6 +309,9 @@
 datatype lexicon = Lexicon of (bool * lexicon) Symtab.table;
 
 val empty_lexicon = Lexicon Symtab.empty;
+
+fun build_lexicon f : lexicon = f empty_lexicon;
+
 fun is_empty_lexicon (Lexicon tab) = Symtab.is_empty tab;
 
 fun is_literal _ [] = false