unused;

--- a/src/Pure/General/bytes.scala	Fri May 11 19:57:49 2018 +0200
+++ b/src/Pure/General/bytes.scala	Fri May 11 19:59:05 2018 +0200
@@ -40,22 +40,6 @@
     }
 
 
-  def hex(s: String): Bytes =
-  {
-    def err(): Nothing = error("Malformed hexadecimal representation of bytes\n" + s)
-    val len = s.length
-    if (len % 2 != 0) err()
-
-    val n = len / 2
-    val a = new Array[Byte](n)
-    for (i <- 0 until n) {
-      val j = 2 * i
-      try { a(i) = Integer.parseInt(s.substring(j, j + 2), 16).toByte }
-      catch { case _: NumberFormatException => err() }
-    }
-    new Bytes(a, 0, n)
-  }
-
   def base64(s: String): Bytes =
   {
     val a = Base64.getDecoder.decode(s)

--- a/src/Pure/library.ML	Fri May 11 19:57:49 2018 +0200
+++ b/src/Pure/library.ML	Fri May 11 19:59:05 2018 +0200
@@ -155,7 +155,6 @@
   val translate_string: (string -> string) -> string -> string
   val encode_lines: string -> string
   val decode_lines: string -> string
-  val hex_string: string -> string
   val align_right: string -> int -> string -> string
   val match_string: string -> string -> bool
 
@@ -777,12 +776,6 @@
 val encode_lines = translate_string (fn "\n" => "\v" | c => c);
 val decode_lines = translate_string (fn "\v" => "\n" | c => c);
 
-fun hex_string s =
-  fold_string (fn c =>
-    let val (a, b) = IntInf.divMod (ord c, 16)
-    in cons (hex_digit a) #> cons (hex_digit b) end) s []
-  |> rev |> implode;
-
 fun align_right c k s =
   let
     val _ = if size c <> 1 orelse size s > k