# HG changeset patch
# User wenzelm
# Date 1135347416 -3600
# Node ID 6574d62fe76ba7e5be462c6eb2001eaf13cb3d8a
# Parent  841137f20307a6f615ca006c3b78403589d0c310
backpatching of Substring.full;

diff -r 841137f20307 -r 6574d62fe76b src/Pure/ML-Systems/polyml.ML
--- 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 *)