diff -r bd57acd44fc1 -r 83060e826e02 etc/settings
--- a/etc/settings	Wed Jul 05 18:27:55 2000 +0200
+++ b/etc/settings	Thu Jul 06 00:08:24 2000 +0200
@@ -27,16 +27,16 @@
 #ML_OPTIONS="@SMLdebug=/dev/null"
 #ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX)
 
-# MLWorks 2.0 or later
-#ML_SYSTEM=mlworks
-#ML_HOME=/usr/local/mlworks/bin
-#ML_OPTIONS=""
+# Moscow ML 2.00 or later (experimental!)
+#ML_SYSTEM=mosml
+#ML_HOME=$ISABELLE_HOME/../mosml/bin
 #ML_PLATFORM=""
+#ML_OPTIONS=""
 
-# Poly/ML 2.x
-#ML_SYSTEM=polyml-2.07
-#ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
-#ML_OPTIONS="-h 30000"
+# MLWorks 2.0
+#ML_SYSTEM=mlworks
+#ML_HOME=$ISABELLE_HOME/../mlworks/bin
+#ML_OPTIONS=""
 #ML_PLATFORM=""
 
 # Standard ML of New Jersey 0.93