src/HOL/Tools/string_syntax.ML

 
 fun char_ast_tr [Ast.Variable xstr] =
       (case Lexicon.explode_xstr xstr of
         [c] => mk_char c
       | _ => error ("Single character expected: " ^ xstr))
+  | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
+      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
   | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
 
 fun char_ast_tr' [c1, c2] =
       Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
   | char_ast_tr' _ = raise Match;

         [] =>
           Ast.Appl
             [Ast.Constant @{syntax_const "_constrain"},
               Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
       | cs => mk_string cs)
+  | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
+      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
   | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
 
 fun list_ast_tr' [args] =
       Ast.Appl [Ast.Constant @{syntax_const "_String"},
         syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]