# HG changeset patch
# User haftmann
# Date 1536394147 0
# Node ID bcce5967e10ebf2ec946127e6c866dd1969fb5c3
# Parent  a0b19a163f5ee3276006e878eb49d2ff9647b685
more explicit notion of ord value for HOL characters

diff -r a0b19a163f5e -r bcce5967e10e src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Sat Sep 08 08:08:28 2018 +0000
+++ b/src/HOL/Tools/string_syntax.ML	Sat Sep 08 08:09:07 2018 +0000
@@ -8,6 +8,7 @@
   val hex: int -> string
   val mk_bits_syntax: int -> int -> term list
   val dest_bits_syntax: term list -> int
+  val ascii_ord_of: string -> int
   val plain_strings_of: string -> string list
   datatype character = Char of string | Ord of int
   val classify_character: int -> character
@@ -47,14 +48,14 @@
 
 (* char *)
 
+fun ascii_ord_of c =
+  if Symbol.is_ascii c then ord c
+  else if c = "\<newline>" then 10
+  else error ("Bad character: " ^ quote c);
+
 fun mk_char_syntax i =
   list_comb (Syntax.const @{const_syntax Char}, mk_bits_syntax 8 i);
 
-fun mk_char_syntax' c =
-  if Symbol.is_ascii c then mk_char_syntax (ord c)
-  else if c = "\<newline>" then mk_char_syntax 10
-  else error ("Bad character: " ^ quote c);
-
 fun plain_strings_of str =
   map fst (Lexicon.explode_str (str, Position.none));
 
@@ -84,7 +85,7 @@
       c $ char_tr [t] $ u
   | char_tr [Free (str, _)] =
       (case plain_strings_of str of
-        [c] => mk_char_syntax' c
+        [c] => mk_char_syntax (ascii_ord_of c)
       | _ => error ("Single character expected: " ^ str))
   | char_tr ts = raise TERM ("char_tr", ts);
 
@@ -107,7 +108,8 @@
 
 fun mk_string_syntax [] = Syntax.const @{const_syntax Nil}
   | mk_string_syntax (c :: cs) =
-      Syntax.const @{const_syntax Cons} $ mk_char_syntax' c $ mk_string_syntax cs;
+      Syntax.const @{const_syntax Cons} $ mk_char_syntax (ascii_ord_of c)
+        $ mk_string_syntax cs;
 
 fun mk_string_ast ss =
   Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},