# HG changeset patch
# User wenzelm
# Date 1204827688 -3600
# Node ID c7d0cd2c7715d79089cbe69aafe47e1996ccaea7
# Parent  94d32a7cd0fb9c1668c243d8c534f906a9719d37
renamed polyml-old-basis.ML to polyml_old_basis.ML;

diff -r 94d32a7cd0fb -r c7d0cd2c7715 src/Pure/ML-Systems/polyml-old-basis.ML
--- a/src/Pure/ML-Systems/polyml-old-basis.ML	Thu Mar 06 19:21:26 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      Pure/ML-Systems/polyml-old-basis.ML
-    ID:         $Id$
-
-Fixes for the old SML basis library (before Poly/ML 4.2.0).
-*)
-
-structure String =
-struct
-  fun isSuffix s1 s2 =
-    let val n1 = size s1 and n2 = size s2
-    in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
-  fun isSubstring s1 s2 =
-    String.isPrefix s1 s2 orelse
-      size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); 
-  open String;
-end;
-
-structure Substring =
-struct
-  open Substring;
-  val full = all;
-end;
-
-structure Posix =
-struct
-  open Posix;
-  structure IO =
-  struct
-    open IO;
-    val mkTextReader = mkReader;
-    val mkTextWriter = mkWriter;
-  end;
-end;
-
-structure TextIO =
-struct
-  open TextIO;
-  fun inputLine is =
-    let val s = TextIO.inputLine is
-    in if s = "" then NONE else SOME s end;
-end;
diff -r 94d32a7cd0fb -r c7d0cd2c7715 src/Pure/ML-Systems/polyml_old_basis.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml_old_basis.ML	Thu Mar 06 19:21:28 2008 +0100
@@ -0,0 +1,41 @@
+(*  Title:      Pure/ML-Systems/polyml_old_basis.ML
+    ID:         $Id$
+
+Fixes for the old SML basis library (before Poly/ML 4.2.0).
+*)
+
+structure String =
+struct
+  fun isSuffix s1 s2 =
+    let val n1 = size s1 and n2 = size s2
+    in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
+  fun isSubstring s1 s2 =
+    String.isPrefix s1 s2 orelse
+      size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); 
+  open String;
+end;
+
+structure Substring =
+struct
+  open Substring;
+  val full = all;
+end;
+
+structure Posix =
+struct
+  open Posix;
+  structure IO =
+  struct
+    open IO;
+    val mkTextReader = mkReader;
+    val mkTextWriter = mkWriter;
+  end;
+end;
+
+structure TextIO =
+struct
+  open TextIO;
+  fun inputLine is =
+    let val s = TextIO.inputLine is
+    in if s = "" then NONE else SOME s end;
+end;