diff -r 0015a0a99ae9 -r dc4f61a7918a src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Thu Feb 11 21:33:25 2010 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Thu Feb 11 22:03:15 2010 +0100
@@ -401,7 +401,7 @@
    Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
    Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
    Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
-  []
+  standard_token_markers
   ([], [], [], [])
   []
   ([], []);