equal
deleted
inserted
replaced
115 |
115 |
116 fun string_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = |
116 fun string_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = |
117 c $ string_tr [t] $ u |
117 c $ string_tr [t] $ u |
118 | string_tr [Free (str, _)] = |
118 | string_tr [Free (str, _)] = |
119 mk_string_syntax (plain_strings_of str) |
119 mk_string_syntax (plain_strings_of str) |
120 | string_tr ts = raise TERM ("char_tr", ts); |
120 | string_tr ts = raise TERM ("string_tr", ts); |
121 |
121 |
122 fun list_ast_tr' [args] = |
122 fun list_ast_tr' [args] = |
123 Ast.Appl [Ast.Constant @{syntax_const "_String"}, |
123 Ast.Appl [Ast.Constant @{syntax_const "_String"}, |
124 (mk_string_ast o maps dest_char_ast o Ast.unfold_ast @{syntax_const "_args"}) args] |
124 (mk_string_ast o maps dest_char_ast o Ast.unfold_ast @{syntax_const "_args"}) args] |
125 | list_ast_tr' _ = raise Match; |
125 | list_ast_tr' _ = raise Match; |