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