src/Pure/ML/ml_init.ML

--- a/src/Pure/ML/ml_init.ML	Wed Sep 11 12:46:56 2024 +0200
+++ b/src/Pure/ML/ml_init.ML	Wed Sep 11 15:36:14 2024 +0200
@@ -34,4 +34,15 @@
 struct
   open Substring;
   val empty = full "";
+
+local
+  val chars = Vector.tabulate (Char.maxOrd, Substring.full o String.str o Char.chr);
+in
+  fun full str =
+    (case String.size str of
+      0 => empty
+    | 1 => Vector.sub (chars, Char.ord (String.sub (str, 0)))
+    | _ => Substring.full str);
 end;
+
+end;