tuned output;
authorwenzelm
Thu, 03 Jan 2019 16:53:18 +0100
changeset 69583 b0568a9dd160
parent 69582 7be690202fc3
child 69584 a91e32843310
tuned output;
src/Pure/Syntax/mixfix.ML
--- 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 "[" "]";