diff -r 1c93cfa807bc -r 715566791eb0 src/Tools/Metis/metis_env.ML
--- 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;
+