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