author | wenzelm |
Sat, 04 Nov 2006 19:25:43 +0100 | |
changeset 21176 | 5ec545dbad6f |
parent 21175 | 98c0405f5493 |
child 21177 | e8228486aa03 |
--- 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;