# HG changeset patch
# User wenzelm
# Date 1727263972 -7200
# Node ID 12994047862fed24e72128b2724109cb02cea281
# Parent  7f028e2ca7db247cf758eba52102d052d25b115d
more markup;

diff -r 7f028e2ca7db -r 12994047862f src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Sep 25 13:30:04 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Sep 25 13:32:52 2024 +0200
@@ -212,8 +212,8 @@
 local
 
 val par_block = Syntax_Ext.block_indent 1;
-val par_bg = make_string "(";
-val par_en = make_string ")";
+val par_bg = make_literal "(";
+val par_en = make_literal ")";
 
 in