diff -r 8fc15183f549 -r 8ce58492bf50 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Jun 02 11:55:18 1999 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Jun 02 22:25:57 1999 +0200
@@ -197,7 +197,8 @@
   ("",             "id => logic",                   Delimfix "_"),
   ("",             "longid => logic",               Delimfix "_"),
   ("",             "var => logic",                  Delimfix "_"),
-  ("_BIND",        "id => logic",                   Delimfix "??_")];
+  ("_BIND",        "id => logic",                   Delimfix "??_"),
+  ("_DDDOT",       "logic",                         Delimfix "...")];
 
 val pure_appl_syntax =
  [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)),