renamed metis-env to metis-env.ML;

--- a/src/Tools/Metis/make-metis	Wed Jun 20 23:19:18 2007 +0200
+++ b/src/Tools/Metis/make-metis	Thu Jun 21 12:01:27 2007 +0200
@@ -40,7 +40,7 @@
     else
       echo -e "$FILE (local)" >&2
       echo "structure Metis = struct open Metis"
-      cat < "metis-env"
+      cat < "metis-env.ML"
       "$THIS/scripts/mlpp" -c isabelle "src/$FILE"
       echo "end;"
     fi

--- a/src/Tools/Metis/metis-env	Wed Jun 20 23:19:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
-val explode = String.explode;
-val implode = String.implode;
-val print = TextIO.print;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/metis-env.ML	Thu Jun 21 12:01:27 2007 +0200
@@ -0,0 +1,5 @@
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;