# HG changeset patch
# User wenzelm
# Date 1182420087 -7200
# Node ID 020381339d8771663f5668af1bda0bb06d0b185b
# Parent  1f16190e38365737fd5e1bfe1b87c717530d0c60
renamed metis-env to metis-env.ML;

diff -r 1f16190e3836 -r 020381339d87 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
diff -r 1f16190e3836 -r 020381339d87 src/Tools/Metis/metis-env
--- 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;
diff -r 1f16190e3836 -r 020381339d87 src/Tools/Metis/metis-env.ML
--- /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;