diff -r 43c4817375bf -r 232a839ef8e6 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 18:38:44 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 20:21:04 2024 +0200
@@ -620,7 +620,7 @@
           in (t1' $ t2', seen'') end;
   in #1 (prune (tm, [])) end;
 
-fun mark_atoms is_syntax_const ctxt tm =
+fun mark_atoms ctxt tm =
   let
     val {structs, fixes} = Syntax_Trans.get_idents ctxt;
     val show_structs = Config.get ctxt show_structs;
@@ -631,7 +631,7 @@
       | mark (t $ u) = mark t $ mark u
       | mark (Abs (x, T, t)) = Abs (x, T, mark t)
       | mark (t as Const (c, T)) =
-          if is_syntax_const c then t
+          if Proof_Context.is_syntax_const ctxt c then t
           else Const (Lexicon.mark_const c, T)
       | mark (t as Free (x, T)) =
           let val i = find_index (fn s => s = x) structs + 1 in
@@ -651,8 +651,6 @@
 
 fun term_to_ast ctxt trf tm =
   let
-    val is_syntax_const = Syntax.is_const (Proof_Context.syntax_of ctxt);
-
     val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
     val show_markup = Config.get ctxt show_markup;
 
@@ -694,7 +692,7 @@
     |> mark_aprop
     |> show_types ? prune_types
     |> Variable.revert_bounds ctxt
-    |> mark_atoms is_syntax_const ctxt
+    |> mark_atoms ctxt
     |> ast_of
   end;