# HG changeset patch
# User haftmann
# Date 1536394147 0
# Node ID 25b431feb2e9df0eaae67c34d14caa1f43ae9cc3
# Parent  bcce5967e10ebf2ec946127e6c866dd1969fb5c3
more appropriate conversion of HOL character literals to character codes: symbolic newline is interpreted as 0x10

diff -r bcce5967e10e -r 25b431feb2e9 src/HOL/Tools/literal.ML
--- a/src/HOL/Tools/literal.ML	Sat Sep 08 08:09:07 2018 +0000
+++ b/src/HOL/Tools/literal.ML	Sat Sep 08 08:09:07 2018 +0000
@@ -36,7 +36,7 @@
 fun literal_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
       c $ literal_tr [t] $ u
   | literal_tr [Free (str, _)] =
-      (mk_literal_syntax o map ord o String_Syntax.plain_strings_of) str
+      (mk_literal_syntax o map String_Syntax.ascii_ord_of o String_Syntax.plain_strings_of) str
   | literal_tr ts = raise TERM ("literal_tr", ts);
 
 fun ascii k = Syntax.const @{syntax_const "_Ascii"}