diff -r 08e0d3f248f9 -r 89ea66c2045b src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Oct 24 11:50:20 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Oct 24 12:42:41 2024 +0200
@@ -160,7 +160,7 @@
   | parsetree_literals (Parser.Tip tok) =
       if Lexicon.is_literal tok andalso
         not (null (Lexicon.literal_markup (Lexicon.str_of_token tok)))
-      then [Lexicon.pos_of_token tok] else [];
+      then filter Position.is_reported [Lexicon.pos_of_token tok] else [];
 
 fun parsetree_to_ast ctxt trf parsetree =
   let
@@ -223,7 +223,7 @@
             val ps = maps parsetree_literals pts;
             val args = maps asts_of pts;
             fun head () =
-              if (Lexicon.is_fixed a orelse Lexicon.is_const a)
+              if not (null ps) andalso (Lexicon.is_fixed a orelse Lexicon.is_const a)
                 andalso not (Config.get ctxt const_syntax_legacy)
               then Ast.constrain (Ast.Constant a) (ast_of_pos ps)
               else Ast.Constant a;