# HG changeset patch
# User wenzelm
# Date 1546530798 -3600
# Node ID b0568a9dd1607be13d723d5c1fa01925a8606973
# Parent  7be690202fc341716e0f801fc6c0a0aed71e86a1
tuned output;

diff -r 7be690202fc3 -r b0568a9dd160 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 "[" "]";