# HG changeset patch
# User wenzelm
# Date 1728737746 -7200
# Node ID 1e7b60cb7694b0c749c9d0cbe63ef1e5be484fb1
# Parent  a311b9da9d9cb2870c73433c9993c1fcf62c6248
tuned;

diff -r a311b9da9d9c -r 1e7b60cb7694 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat Oct 12 14:48:10 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat Oct 12 14:55:46 2024 +0200
@@ -277,20 +277,22 @@
       (case transT a args p of
         SOME res => res
       | NONE =>
+          (*find matching table entry, or print as prefix / postfix*)
           let
             val nargs = length args;
-
-            (*find matching table entry, or print as prefix / postfix*)
-            fun prnt ([], []) =
-                  if nargs = 0 then [atomT a]
-                  else astT (appT (c, args), p)
-              | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
-              | prnt ((pr, n, p') :: prnps, tbs) =
-                  if nargs = n then parT (#1 markup_extern a) (pr, args, p, p')
-                  else if nargs > n andalso not type_mode then
-                    astT (appT (splitT n ([c], args)), p)
-                  else prnt (prnps, tbs);
-          in prnt ([], tabs) end)
+            val entry =
+              tabs |> get_first (fn tab =>
+                Symtab.lookup_list tab a |> find_first (fn (_, n, _) =>
+                  nargs = n orelse nargs > n andalso not type_mode));
+          in
+            (case entry of
+              NONE =>
+                if nargs = 0 then [atomT a]
+                else astT (appT (c, args), p)
+            | SOME (pr, n, p') =>
+                if nargs = n then parT (#1 markup_extern a) (pr, args, p, p')
+                else astT (appT (splitT n ([c], args)), p))
+          end)
 
     and astT (Ast.Variable x, _) = [Ast.pretty_var x]
       | astT (c as Ast.Constant a, p) = combT c a [] p