String.isPrefix

--- a/src/Pure/ML-Systems/polyml.ML	Mon Aug 02 11:31:04 1999 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Aug 02 11:33:18 1999 +0200
@@ -16,6 +16,8 @@
   struct
   fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j)
                           handle Substring => raise Subscript
+  fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
+                       handle Subscript => false
   val concat = implode
   end;