# HG changeset patch
# User wenzelm
# Date 1727614549 -7200
# Node ID 3668aec7afa2e0744069b5888ae8f58c2849cd83
# Parent  6bc70ba0636fd5754ab40bd208c1dd6225d8b740
tuned;

diff -r 6bc70ba0636f -r 3668aec7afa2 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Sep 29 13:48:34 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Sep 29 14:55:49 2024 +0200
@@ -161,6 +161,11 @@
       if Lexicon.is_literal tok andalso null (Lexicon.literal_markup (Lexicon.str_of_token tok))
       then Position.none else Lexicon.pos_of_token tok;
 
+    fun report_token a (Parser.Tip tok) =
+          if Lexicon.valued_token tok then ()
+          else report (report_pos tok) (markup_entity ctxt) a
+      | report_token _ _ = ();
+
     fun trans a args =
       (case trf a of
         NONE => Ast.mk_appl (Ast.Constant a) args
@@ -204,11 +209,7 @@
       | asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) =
           [Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)]
       | asts_of (Parser.Node (a, pts)) =
-          let
-            val _ = pts |> List.app
-              (fn Parser.Node _ => () | Parser.Tip tok =>
-                if Lexicon.valued_token tok then ()
-                else report (report_pos tok) (markup_entity ctxt) a);
+          let val _ = List.app (report_token a) pts;
           in [trans a (maps asts_of pts)] end
       | asts_of (Parser.Tip tok) = asts_of_token tok