# HG changeset patch
# User blanchet
# Date 1284560522 -7200
# Node ID 27f5ee6b91010140dbe12ea679667a206a5f2fcf
# Parent  0be01cad5df4d456ad4cd3259fba88d7a800edae
no need for "metis_env.ML" anymore;
it was a neat solution but it didn't work anymore once I removed the "structure Metis"

diff -r 0be01cad5df4 -r 27f5ee6b9101 src/Tools/Metis/metis_env.ML
--- 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;
-