src/Pure/Syntax/syntax_phases.ML

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Mar 30 16:36:23 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Mar 30 17:03:26 2016 +0200
@@ -624,7 +624,7 @@
             else Syntax.const "_free" $ t
           end
       | mark (t as Var (xi, T)) =
-          if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
+          if xi = Auto_Bind.dddot then Const ("_DDDOT", T)
           else Syntax.const "_var" $ t
       | mark a = a;
   in mark tm end;