src/Pure/ML/ml_init.ML

--- a/src/Pure/ML/ml_init.ML	Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/ML/ml_init.ML	Wed Jun 22 17:07:00 2022 +0200
@@ -33,3 +33,9 @@
     if n = 1 then String.str (String.sub (s, i))
     else String.substring (s, i, n);
 end;
+
+structure Substring =
+struct
+  open Substring;
+  val empty = full "";
+end;