# HG changeset patch
# User wenzelm
# Date 1182426833 -7200
# Node ID 95b70054bb3a7c17fa572650f803c8864189496e
# Parent  51c23b0929fba23c18799f98326034caf3c0821e
renamed metis-env.ML to metis_env.ML;

diff -r 51c23b0929fb -r 95b70054bb3a src/Tools/Metis/make-metis
--- a/src/Tools/Metis/make-metis	Thu Jun 21 13:53:23 2007 +0200
+++ b/src/Tools/Metis/make-metis	Thu Jun 21 13:53:53 2007 +0200
@@ -11,6 +11,8 @@
 THIS=$(cd "$(dirname "$0")"; echo $PWD)
 
 (
+  echo -n '(* $'
+  echo 'Id$ *)'
   cat <<EOF
 (******************************************************************)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
@@ -40,7 +42,7 @@
     else
       echo -e "$FILE (local)" >&2
       echo "structure Metis = struct open Metis"
-      cat < "metis-env.ML"
+      cat < "metis_env.ML"
       "$THIS/scripts/mlpp" -c isabelle "src/$FILE"
       echo "end;"
     fi
diff -r 51c23b0929fb -r 95b70054bb3a src/Tools/Metis/metis-env.ML
--- a/src/Tools/Metis/metis-env.ML	Thu Jun 21 13:53:23 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 51c23b0929fb -r 95b70054bb3a 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 13:53:53 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;