diff -r 82aaa0d8fc3b -r 84f2d481d6d7 etc/settings
--- a/etc/settings	Thu Mar 21 12:47:51 2024 +0100
+++ b/etc/settings	Thu Mar 21 14:19:05 2024 +0100
@@ -185,7 +185,5 @@
 ISABELLE_GNUPLOT="gnuplot"
 ISABELLE_FONTFORGE="fontforge"
 
-#ISABELLE_MLTON="/usr/bin/mlton"
-#ISABELLE_MLTON_OPTIONS="-pi-style npi"
 #ISABELLE_SMLNJ="/usr/bin/sml"
 #ISABELLE_SWIPL="/usr/bin/swipl"