src/Tools/Metis/metis_env.ML

--- a/src/Tools/Metis/metis_env.ML	Wed Sep 15 16:35:49 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;
-