# HG changeset patch
# User wenzelm
# Date 1729100642 -7200
# Node ID 3c262e273ebdc758de48cfe8ac1a5b983a66522a
# Parent  6002cb6bfb0ac08076af850291c4435fef935e6f
tuned signature;

diff -r 6002cb6bfb0a -r 3c262e273ebd src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Oct 16 16:20:35 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Oct 16 19:44:02 2024 +0200
@@ -69,7 +69,7 @@
 
 datatype symb =
   Arg of int |
-  TypArg of int |
+  Arg_Type of int |
   String of Markup.T list * string |
   Break of int |
   Block of Syntax_Ext.block * symb list;
@@ -89,7 +89,7 @@
 local
 
 fun is_arg (Arg _) = true
-  | is_arg (TypArg _) = true
+  | is_arg (Arg_Type _) = true
   | is_arg _ = false;
 
 fun is_space str = forall_string (fn s => s = " ") str;
@@ -120,7 +120,7 @@
   |> map_filter (fn (symbs, _, p) =>
       (case clean symbs of
         [Arg p1, String (_, d), Arg p2] => SOME (p1, p2, d, p)
-      | [TypArg p1, String (_, d), TypArg p2] => SOME (p1, p2, d, p)
+      | [Arg_Type p1, String (_, d), Arg_Type p2] => SOME (p1, p2, d, p)
       | _ => NONE))
   |> get_first (fn (p1, p2, d, p) =>
       if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = d, pri = p}
@@ -137,7 +137,7 @@
 fun make_literal s = String (Lexicon.literal_markup s, s);
 
 fun make_arg (s, p) =
-  (if s = "type" then TypArg else Arg)
+  (if s = "type" then Arg_Type else Arg)
   (if Lexicon.is_terminal s then 1000 else p);
 
 fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
@@ -156,7 +156,7 @@
           | make_symbs [] = ([], []);
 
         fun count_args (Arg _ :: syms) = Integer.add 1 #> count_args syms
-          | count_args (TypArg _ :: syms) = Integer.add 1 #> count_args syms
+          | count_args (Arg_Type _ :: syms) = Integer.add 1 #> count_args syms
           | count_args (String _ :: syms) = count_args syms
           | count_args (Break _ :: syms) = count_args syms
           | count_args (Block (_, bsyms) :: syms) = count_args syms #> count_args bsyms
@@ -294,7 +294,7 @@
       | syntax m (Arg p :: symbs, arg :: args) =
           let val (prts, args') = syntax m (symbs, args);
           in (main p arg @ prts, args') end
-      | syntax m (TypArg p :: symbs, arg :: args) =
+      | syntax m (Arg_Type p :: symbs, arg :: args) =
           let val (prts, args') = syntax m (symbs, args);
           in (main_type p arg @ prts, args') end
       | syntax m (String (literal_markup, s) :: symbs, args) =