| changeset 69349 | 7cef9e386ffe |
| parent 69064 | 5840724b1d71 |
| child 69582 | 7be690202fc3 |
--- a/src/Pure/Syntax/mixfix.ML Tue Nov 27 16:22:12 2018 +0100 +++ b/src/Pure/Syntax/mixfix.ML Tue Nov 27 21:07:39 2018 +0100 @@ -87,7 +87,7 @@ local -val quoted = Pretty.quote o Pretty.str o Input.source_content; +val quoted = Pretty.quote o Pretty.str o #1 o Input.source_content; val keyword = Pretty.keyword2; val parens = Pretty.enclose "(" ")"; val brackets = Pretty.enclose "[" "]";