src/Pure/ML/ml_init.ML

   open String;
   fun substring (s, i, n) =
     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;