src/Pure/General/symbol.ML

   val malformed: symbol
   val end_malformed: symbol
   val is_regular: symbol -> bool
   val is_ascii: symbol -> bool
   val is_ascii_letter: symbol -> bool
-  val is_hex_letter: symbol -> bool
   val is_ascii_digit: symbol -> bool
+  val is_ascii_hex: symbol -> bool
   val is_ascii_quasi: symbol -> bool
   val is_ascii_blank: symbol -> bool
   val is_ascii_lower: symbol -> bool
   val is_ascii_upper: symbol -> bool
   val to_ascii_lower: symbol -> symbol

 fun is_ascii_letter s =
   is_char s andalso
    (ord "A" <= ord s andalso ord s <= ord "Z" orelse
     ord "a" <= ord s andalso ord s <= ord "z");
 
-fun is_hex_letter s =
-  is_char s andalso
-   (ord "A" <= ord s andalso ord s <= ord "F" orelse
-    ord "a" <= ord s andalso ord s <= ord "f");
-
 fun is_ascii_digit s =
   is_char s andalso ord "0" <= ord s andalso ord s <= ord "9";
+
+fun is_ascii_hex s =
+  is_char s andalso
+   (ord "0" <= ord s andalso ord s <= ord "9" orelse
+    ord "A" <= ord s andalso ord s <= ord "F" orelse
+    ord "a" <= ord s andalso ord s <= ord "f");
 
 fun is_ascii_quasi "_" = true
   | is_ascii_quasi "'" = true
   | is_ascii_quasi _ = false;
 
 val is_ascii_blank =
-  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\^M" => true
+  fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\^L" => true | "\^M" => true
     | _ => false;
 
 fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");
 fun is_ascii_upper s = is_char s andalso (ord "A" <= ord s andalso ord s <= ord "Z");