| changeset 68099 | 305f9f3edf05 |
| parent 68028 | 1f9f973eed2a |
| child 68939 | bcce5967e10e |
--- a/src/HOL/Tools/string_syntax.ML Sun May 06 18:20:25 2018 +0000 +++ b/src/HOL/Tools/string_syntax.ML Sun May 06 18:20:25 2018 +0000 @@ -117,7 +117,7 @@ c $ string_tr [t] $ u | string_tr [Free (str, _)] = mk_string_syntax (plain_strings_of str) - | string_tr ts = raise TERM ("char_tr", ts); + | string_tr ts = raise TERM ("string_tr", ts); fun list_ast_tr' [args] = Ast.Appl [Ast.Constant @{syntax_const "_String"},