--- a/src/Pure/ML-Systems/polyml.ML Fri Dec 23 15:16:55 2005 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Fri Dec 23 15:16:56 2005 +0100
@@ -18,6 +18,12 @@
open String;
end;
+structure Substring =
+struct
+ open Substring;
+ val full = all;
+end;
+
(* cygwin *)