# HG changeset patch
# User wenzelm
# Date 1725212130 -7200
# Node ID 5e38e8b34eb35e590e3e9ad4373d3742e496cabd
# Parent  d4c489401844459ddcd4830c8bfab56e773b919e
proper string syntax (amending 70076ba563d2);

diff -r d4c489401844 -r 5e38e8b34eb3 src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Sat Aug 31 16:01:36 2024 +0200
+++ b/src/HOL/Tools/string_syntax.ML	Sun Sep 01 19:35:30 2024 +0200
@@ -123,7 +123,7 @@
 
 fun list_ast_tr' [args] =
       Ast.Appl [Ast.Constant \<^syntax_const>\<open>_String\<close>,
-        (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\<open>_args\<close>) args]
+        (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\<open>_list_args\<close>) args]
   | list_ast_tr' _ = raise Match;