no need for "metis_env.ML" anymore;
it was a neat solution but it didn't work anymore once I removed the "structure Metis"

--- a/src/Tools/Metis/metis_env.ML	Wed Sep 15 16:20:46 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(* Metis-specific ML environment *)
-nonfix ++ -- RL;
-val explode = String.explode;
-val implode = String.implode;
-val print = TextIO.print;
-val foldl = List.foldl;
-val foldr = List.foldr;
-