# HG changeset patch
# User wenzelm
# Date 1162664743 -3600
# Node ID 5ec545dbad6fbcd95b77aa4a6c43d839b76eb335
# Parent  98c0405f54933b503ea9c4edb7303b0fc0a749d2
String.compare: slow version -- performance test;

diff -r 98c0405f5493 -r 5ec545dbad6f 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;