diff -r 5cb40c8b1f10 -r e26915e01d15 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Mon Aug 01 19:20:21 2005 +0200
+++ b/lib/scripts/run-polyml	Mon Aug 01 19:20:22 2005 +0200
@@ -100,6 +100,14 @@
 
 ## run it!
 
+case "$ML_SYSTEM" in
+  polyml-4.1.[12])
+    ;;
+  polyml-4.1.*)
+    MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $MLTEXT"
+    ;;
+esac
+
 if [ -z "$TERMINATE" ]; then
   FEEDER_OPTS=""
 else