src/Pure/ML-Systems/polyml-4.9.1.ML

--- a/src/Pure/ML-Systems/polyml-4.9.1.ML	Sat Nov 04 19:25:41 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-4.9.1.ML	Sat Nov 04 19:25:43 2006 +0100
@@ -9,3 +9,14 @@
 use "ML-Systems/polyml.ML";
 
 val pointer_eq = PolyML.pointerEq;
+
+(* FIXME slow version -- performance test *)
+structure String =
+struct
+  open String;
+
+  fun compare (s1: string, s2) =
+    if s1 = s2 then General.EQUAL
+    else if s1 < s2 then General.LESS
+    else General.GREATER;
+end;