src/HOL/Tools/string_syntax.ML
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"},