diff -r ec1023a5c54c -r 179a24b40200 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Aug 22 17:12:32 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Aug 23 13:28:01 2024 +0200
@@ -77,7 +77,7 @@
   val eq_syntax: syntax * syntax -> bool
   datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}
   val get_approx: syntax -> string -> approx option
-  val lookup_const: syntax -> string -> string option
+  val get_const: syntax -> string -> string
   val is_const: syntax -> string -> bool
   val is_keyword: syntax -> string -> bool
   val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
@@ -441,7 +441,6 @@
       | NONE => Printer.get_binder prtabs c)
       |> Option.map Prefix);
 
-fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
 fun is_const (Syntax ({consts, ...}, _)) = Symtab.defined consts;
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
@@ -468,6 +467,23 @@
   Synchronized.cache (fn () => Parser.make_gram new_xprods [] NONE);
 
 
+(* syntax consts *)
+
+fun get_const (Syntax ({consts, ...}, _)) =
+  let
+    fun get c =
+      (case Symtab.lookup consts c of
+        NONE => c
+      | SOME "" => c
+      | SOME b => get b);
+  in get end;
+
+fun update_const (c, b) tab =
+  if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c))
+  then tab
+  else Symtab.update (c, b) tab;
+
+
 (* empty_syntax *)
 
 val empty_syntax = Syntax
@@ -487,11 +503,6 @@
 
 (* update_syntax *)
 
-fun update_const (c, b) tab =
-  if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c))
-  then tab
-  else Symtab.update (c, b) tab;
-
 fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   let
     val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab,