diff -r 60801e5fae26 -r dad0cefb48dd src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Aug 22 15:57:30 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Aug 22 16:04:06 2024 +0200
@@ -648,8 +648,10 @@
 
 in
 
-fun term_to_ast is_syntax_const ctxt trf tm =
+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;
 
@@ -801,12 +803,8 @@
 fun unparse_term ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val syn = Proof_Context.syntax_of ctxt;
-  in
-    unparse_t (term_to_ast (Syntax.is_const syn))
-      (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
-      (Markup.language_term false) ctxt
-  end;
+    val curried = not (Pure_Thy.old_appl_syntax thy);
+  in unparse_t term_to_ast (Printer.pretty_term_ast curried) (Markup.language_term false) ctxt end;
 
 end;