src/Pure/Syntax/syn_ext.ML
changeset 35110 dc4f61a7918a
parent 33317 b4534348b8fd
child 35351 7425aece4ee3
--- 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
   ([], [], [], [])
   []
   ([], []);