more appropriate conversion of HOL character literals to character codes: symbolic newline is interpreted as 0x10
authorhaftmann
Sat Sep 08 08:09:07 2018 +0000 (9 months ago)
changeset 6894025b431feb2e9
parent 68939 bcce5967e10e
child 68950 53f7b6b9f734
more appropriate conversion of HOL character literals to character codes: symbolic newline is interpreted as 0x10
src/HOL/Tools/literal.ML
     1.1 --- a/src/HOL/Tools/literal.ML	Sat Sep 08 08:09:07 2018 +0000
     1.2 +++ b/src/HOL/Tools/literal.ML	Sat Sep 08 08:09:07 2018 +0000
     1.3 @@ -36,7 +36,7 @@
     1.4  fun literal_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
     1.5        c $ literal_tr [t] $ u
     1.6    | literal_tr [Free (str, _)] =
     1.7 -      (mk_literal_syntax o map ord o String_Syntax.plain_strings_of) str
     1.8 +      (mk_literal_syntax o map String_Syntax.ascii_ord_of o String_Syntax.plain_strings_of) str
     1.9    | literal_tr ts = raise TERM ("literal_tr", ts);
    1.10  
    1.11  fun ascii k = Syntax.const @{syntax_const "_Ascii"}