diff -r 41e843d901ee -r d2e39f0f9b40 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Oct 27 15:30:00 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Oct 27 19:57:29 2024 +0100
@@ -202,6 +202,8 @@
               |>> dest_Type_name;
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
+      | asts_of (Parser.Node ({const = "_DDDOT", ...}, [Parser.Tip tok])) =
+          [Ast.constrain (Ast.Variable Auto_Bind.dddot_vname) (ast_of_position tok)]
       | asts_of (Parser.Node ({const = "_position", ...}, [Parser.Tip tok])) =
           asts_of_position "_constrain" tok
       | asts_of (Parser.Node ({const = "_position_sort", ...}, [Parser.Tip tok])) =
@@ -662,7 +664,7 @@
             else Syntax.const "_free" $ t
           end
       | mark (t as Var (xi, T)) =
-          if xi = Auto_Bind.dddot then Const ("_DDDOT", T)
+          if xi = Auto_Bind.dddot_indexname then Const ("_DDDOT", T)
           else Syntax.const "_var" $ t
       | mark a = a;
   in mark tm end;