# HG changeset patch
# User wenzelm
# Date 1265922195 -3600
# Node ID dc4f61a7918abf17cd40cdcd6f8a032b58e2dc26
# Parent  0015a0a99ae9f202a3df944fd337ea6012e3d349
treat inner token markers as syntax consts;

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
   ([], [], [], [])
   []
   ([], []);