diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Metis/make-metis
--- a/src/Tools/Metis/make-metis	Tue Sep 29 14:59:24 2009 +0200
+++ b/src/Tools/Metis/make-metis	Tue Sep 29 16:24:36 2009 +0200
@@ -30,16 +30,19 @@
     then
       echo -e "$FILE (global)" >&2
       "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
-      perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;'
+      perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \
+      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
     elif fgrep -q functor "src/$FILE"
     then
       "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
-      perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;'
+      perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \
+      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
     else
       echo -e "$FILE (local)" >&2
       echo "structure Metis = struct open Metis"
       cat < "metis_env.ML"
-      "$THIS/scripts/mlpp" -c isabelle "src/$FILE"
+      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
+      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
       echo "end;"
     fi
   done