--- a/src/Tools/Metis/metis_env.ML Mon Oct 19 23:02:23 2009 +0200
+++ b/src/Tools/Metis/metis_env.ML Mon Oct 19 23:02:56 2009 +0200
@@ -3,3 +3,6 @@
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+