equal
deleted
inserted
replaced
121 mk_string_syntax (plain_strings_of str) |
121 mk_string_syntax (plain_strings_of str) |
122 | string_tr ts = raise TERM ("string_tr", ts); |
122 | string_tr ts = raise TERM ("string_tr", ts); |
123 |
123 |
124 fun list_ast_tr' [args] = |
124 fun list_ast_tr' [args] = |
125 Ast.Appl [Ast.Constant \<^syntax_const>\<open>_String\<close>, |
125 Ast.Appl [Ast.Constant \<^syntax_const>\<open>_String\<close>, |
126 (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\<open>_list_args\<close>) args] |
126 (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\<open>_args\<close>) args] |
127 | list_ast_tr' _ = raise Match; |
127 | list_ast_tr' _ = raise Match; |
128 |
128 |
129 |
129 |
130 (* theory setup *) |
130 (* theory setup *) |
131 |
131 |