--- 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)),