diff -r 2c75267e7b8d -r fcfd07f122d4 src/Tools/Metis/src/Options.sml
--- a/src/Tools/Metis/src/Options.sml	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Options.sml	Thu Mar 24 17:49:27 2011 +0100
@@ -155,7 +155,7 @@
         [{leftAlign = true, padChar = #"."},
          {leftAlign = true, padChar = #" "}]
 
-    val table = alignTable alignment (map listOpts options)
+    val table = alignTable alignment (List.map listOpts options)
   in
     header ^ join "\n" table ^ "\n" ^ footer
   end;