diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Mon Sep 30 13:00:42 2024 +0200 +++ b/src/HOL/Tools/string_syntax.ML Mon Sep 30 20:30:59 2024 +0200 @@ -123,7 +123,7 @@ fun list_ast_tr' [args] = Ast.Appl [Ast.Constant \<^syntax_const>\_String\, - (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\_list_args\) args] + (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\_args\) args] | list_ast_tr' _ = raise Match;