# HG changeset patch
# User wenzelm
# Date 1163197332 -3600
# Node ID 2fbe0044edd99491196d7f4b6215f003e4c45331
# Parent  4b01726d71fc8c836345c672c3bf0a686304d7de
tuned comments;
back to fast String.compare (almost no difference in performance);

diff -r 4b01726d71fc -r 2fbe0044edd9 src/Pure/ML-Systems/polyml-4.9.1.ML
--- 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;