author | wenzelm |
Thu, 03 Jan 2019 16:53:18 +0100 | |
changeset 69583 | b0568a9dd160 |
parent 69582 | 7be690202fc3 |
child 69584 | a91e32843310 |
--- a/src/Pure/Syntax/mixfix.ML Thu Jan 03 16:53:04 2019 +0100 +++ b/src/Pure/Syntax/mixfix.ML Thu Jan 03 16:53:18 2019 +0100 @@ -87,7 +87,7 @@ local -val template = Pretty.quote o Pretty.str o #1 o Input.source_content; +val template = Pretty.cartouche o Pretty.str o #1 o Input.source_content; val keyword = Pretty.keyword2; val parens = Pretty.enclose "(" ")"; val brackets = Pretty.enclose "[" "]";