# HG changeset patch
# User wenzelm
# Date 1727254096 -7200
# Node ID 4d6ce43b663c8b903e98d134a05a7844af6dbb65
# Parent  b4a6bee4621aacbe802d9a280a4d1738547d0d80
tuned signature;

diff -r b4a6bee4621a -r 4d6ce43b663c src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Sep 25 10:38:46 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Sep 25 10:48:16 2024 +0200
@@ -138,24 +138,24 @@
           (if s = "type" then TypArg else Arg)
           (if Lexicon.is_terminal s then 1000 else p);
 
-        fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
+        fun make_symbs (Syntax_Ext.Delim s :: xsyms) =
               apfst (cons (String (not (Lexicon.suppress_literal_markup s), s)))
-                (xsyms_to_syms xsyms)
-          | xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
-              apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
-          | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
-              apfst (cons (String (false, s))) (xsyms_to_syms xsyms)
-          | xsyms_to_syms (Syntax_Ext.Bg block :: xsyms) =
+                (make_symbs xsyms)
+          | make_symbs (Syntax_Ext.Argument s_p :: xsyms) =
+              apfst (cons (arg s_p)) (make_symbs xsyms)
+          | make_symbs (Syntax_Ext.Space s :: xsyms) =
+              apfst (cons (String (false, s))) (make_symbs xsyms)
+          | make_symbs (Syntax_Ext.Bg block :: xsyms) =
               let
-                val (bsyms, xsyms') = xsyms_to_syms xsyms;
-                val (syms, xsyms'') = xsyms_to_syms xsyms';
+                val (bsyms, xsyms') = make_symbs xsyms;
+                val (syms, xsyms'') = make_symbs xsyms';
               in
                 (Block (block, bsyms) :: syms, xsyms'')
               end
-          | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) =
-              apfst (cons (Break i)) (xsyms_to_syms xsyms)
-          | xsyms_to_syms (Syntax_Ext.En :: xsyms) = ([], xsyms)
-          | xsyms_to_syms [] = ([], []);
+          | make_symbs (Syntax_Ext.Brk i :: xsyms) =
+              apfst (cons (Break i)) (make_symbs xsyms)
+          | make_symbs (Syntax_Ext.En :: xsyms) = ([], xsyms)
+          | make_symbs [] = ([], []);
 
         fun nargs (Arg _ :: syms) = nargs syms + 1
           | nargs (TypArg _ :: syms) = nargs syms + 1
@@ -164,7 +164,7 @@
           | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
           | nargs [] = 0;
       in
-        (case xsyms_to_syms xsymbs of
+        (case make_symbs xsymbs of
           (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
         | _ => raise Fail "Unbalanced pretty-printing blocks")
       end;