# HG changeset patch
# User haftmann
# Date 1525630825 0
# Node ID 305f9f3edf059ed6b41b5b5d70f9e143d63cbb1a
# Parent  e2bb1d95cbd06bd4eaf9959fdc1f7ef6a8bdb5fd
typo

diff -r e2bb1d95cbd0 -r 305f9f3edf05 src/HOL/Tools/string_syntax.ML
--- 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"},