diff -r 7e8f49d412d6 -r c70a6c169a16 src/Tools/Metis/make_metis
--- a/src/Tools/Metis/make_metis	Wed Sep 15 15:49:21 2010 +0200
+++ b/src/Tools/Metis/make_metis	Wed Sep 15 15:49:43 2010 +0200
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 #
-# make-metis - turn original Metis files into Isabelle ML source.
+# make_metis - turn original Metis files into Isabelle ML source.
 #
 # Structure declarations etc. are made local by wrapping into a
 # collective structure Metis.  Signature and functor definitions are
@@ -11,7 +11,7 @@
 (
   cat <<EOF
 (*
-   This file was generated by the "make-metis" script. The BSD License is used
+   This file was generated by the "make_metis" script. The BSD License is used
    with Joe Hurd's kind permission. Extract from a September 13, 2010 email
    written by Joe Hurd: