# HG changeset patch
# User wenzelm
# Date 1212001577 -7200
# Node ID aae9b369b338bd64dbb378bf1d34c88e76d90da3
# Parent  215d64dc971e61b4fecc6a7b8f7ac266d9acaf45
added Substring.full;

diff -r 215d64dc971e -r aae9b369b338 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Wed May 28 14:48:50 2008 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Wed May 28 21:06:17 2008 +0200
@@ -53,6 +53,12 @@
   open Int;
 end;
 
+structure Substring =
+struct
+  open Substring;
+  val full = all;
+end;
+
 structure Real =
 struct
   open Real;