author | wenzelm |
Sun, 01 Sep 2024 19:35:30 +0200 | |
changeset 80795 | 5e38e8b34eb3 |
parent 80794 | d4c489401844 |
child 80796 | 12efa7f92f35 |
--- 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;