merged

--- a/lib/Tools/usedir	Sat Dec 13 13:24:45 2008 +0100
+++ b/lib/Tools/usedir	Sat Dec 13 16:29:33 2008 +0100
@@ -40,6 +40,11 @@
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
   echo
+  echo "  ML_PLATFORM=$ML_PLATFORM"
+  echo "  ML_HOME=$ML_HOME"
+  echo "  ML_SYSTEM=$ML_SYSTEM"
+  echo "  ML_OPTIONS=$ML_OPTIONS"
+  echo
   exit 1
 }