Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
treat inner token markers as syntax consts;
authorwenzelm
Thu, 11 Feb 2010 22:03:15 +0100
changeset 35110 dc4f61a7918a
parent 35109 0015a0a99ae9
child 35111 18cd034922ba
treat inner token markers as syntax consts;
src/Pure/Syntax/syn_ext.ML file | annotate | diff | comparison | revisions 
--- 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
   ([], [], [], [])
   []
   ([], []);
isabelle