tuned comments;
back to fast String.compare (almost no difference in performance);

--- a/src/Pure/ML-Systems/polyml-4.9.1.ML	Fri Nov 10 23:22:11 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-4.9.1.ML	Fri Nov 10 23:22:12 2006 +0100
@@ -1,6 +1,5 @@
 (*  Title:      Pure/ML-Systems/polyml-4.9.1.ML
     ID:         $Id$
-    Author:     Makarius
 
 Compatibility wrapper for Poly/ML 4.9.1.
 *)
@@ -9,14 +8,3 @@
 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;