diff -r ee218296d635 -r 028e39e5e8f3 src/Tools/Metis/src/Ordered.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Ordered.sml	Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,10 @@
+(* ========================================================================= *)
+(* ORDERED TYPES                                                             *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure IntOrdered =
+struct type t = int val compare = Int.compare end;
+
+structure StringOrdered =
+struct type t = string val compare = String.compare end;