| changeset 69593 | 3dda49e08b9d |
| parent 69485 | b734ff28e405 |
| child 69659 | 07025152dd80 |
--- a/src/Tools/Code/code_printer.ML Fri Jan 04 21:49:06 2019 +0100 +++ b/src/Tools/Code/code_printer.ML Fri Jan 04 23:22:53 2019 +0100 @@ -400,7 +400,7 @@ end; val parse_fixity = - (@{keyword "infix"} >> K X) || (@{keyword "infixl"} >> K L) || (@{keyword "infixr"} >> K R) + (\<^keyword>\<open>infix\<close> >> K X) || (\<^keyword>\<open>infixl\<close> >> K L) || (\<^keyword>\<open>infixr\<close> >> K R) fun parse_mixfix x = (Parse.string >> read_mixfix