more markup;
authorwenzelm
Wed, 25 Sep 2024 13:32:52 +0200
changeset 80956 12994047862f
parent 80955 7f028e2ca7db
child 80957 8aff3182ef82
more markup;
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