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