author | wenzelm |
Sat, 04 Nov 2006 19:25:43 +0100 | |
changeset 21176 | 5ec545dbad6f |
parent 20816 | 1cf97e0bba57 |
child 21280 | b4aa7daa506b |
permissions | -rw-r--r-- |
(* Title: Pure/ML-Systems/polyml-4.2.0.ML ID: $Id$ Author: Makarius Compatibility wrapper for Poly/ML 4.9.1. *) use "ML-Systems/polyml-4.1.4-patch.ML"; 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;