# HG changeset patch
# User paulson
# Date 933586398 -7200
# Node ID ff492d5d77cc9b95531dbc4ee4363e12f87b2dd2
# Parent  3c664fbb291017d0359c9ddd917540ec406e83e8
String.isPrefix

diff -r 3c664fbb2910 -r ff492d5d77cc src/Pure/ML-Systems/polyml.ML
--- 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;