# 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"}