src/Tools/Metis/make-metis

--- 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