# HG changeset patch
# User blanchet
# Date 1284569508 -7200
# Node ID a28be69dcb68743b6f7e0bc6896037fa0bf18877
# Parent  c551ce5f614a4da3270fb3cf1bab4b31d1973623
update comment

diff -r c551ce5f614a -r a28be69dcb68 src/Tools/Metis/make_metis
--- a/src/Tools/Metis/make_metis	Wed Sep 15 18:51:21 2010 +0200
+++ b/src/Tools/Metis/make_metis	Wed Sep 15 18:51:48 2010 +0200
@@ -2,9 +2,9 @@
 #
 # 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
-# global!
+# Signatures, structures, and functors are renamed to have a "Metis_" prefix.
+# A few other ad hoc transformations are performed to ensure that the sources
+# compile within Isabelle on Poly/ML and SML/NJ.
 
 THIS=$(cd "$(dirname "$0")"; echo $PWD)